diff --git a/src/TransitionSystem.cc b/src/TransitionSystem.cc
index e52e2118..52d6b07f 100644
--- a/src/TransitionSystem.cc
+++ b/src/TransitionSystem.cc
@@ -9,6 +9,8 @@
 
 #include "TermUtils.h"
 #include "QuantifierElimination.h"
+#include "utils/SmtSolver.h"
+#include "utils/Timer.h"
 
 bool TransitionSystem::isWellFormed() {
 //    return systemType->isStateFormula(init) && systemType->isStateFormula(query) && systemType->isTransitionFormula(transition);
@@ -177,8 +179,19 @@ PTRef TransitionSystem::reverseTransitionRelation(TransitionSystem const & trans
     return transition;
 }
 
+PTRef KTo1Inductive::kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) const {
+    switch (mode) {
+        case Mode::UNFOLD:
+            return unfold(invariant, k, system);
+        case Mode::LEGACY:
+            return legacy(invariant, k, system);
+        default:
+            assert(false);
+            throw std::logic_error("Unreachable!");
+    }
+}
 
-PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem const & system) {
+PTRef KTo1Inductive::legacy(PTRef invariant, unsigned k, TransitionSystem const & system) {
     /*
      * If P(x) is k-inductive invariant then the following formula is 1-inductive invariant:
      * P(x_0)
@@ -223,7 +236,7 @@ PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem c
     resArgs.push(logic.mkNot(afterElimination));
     helpers.push(transition);
     // steps 2 to k-1
-    for (unsigned long i = 2; i < k; ++i) {
+    for (unsigned i = 2; i < k; ++i) {
 //        std::cout << "Step " << i << " out of " << k << std::endl;
         PTRef helper = logic.mkAnd({helpers[i-1], getNextVersion(invariant, i-1), getNextVersion(transition, i-1)});
         helper = QuantifierElimination(logic).eliminate(helper, getStateVars(i-1));
@@ -232,4 +245,78 @@ PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem c
         resArgs.push(logic.mkNot(afterElimination));
     }
     return logic.mkAnd(std::move(resArgs));
+}
+
+namespace {
+
+PTRef buildFormula(unsigned index, PTRef invariant, TransitionSystem const & system) {
+    if (index == 0) { return system.getLogic().getTerm_true(); }
+    Logic & logic = system.getLogic();
+    TimeMachine timeMachine(logic);
+    PTRef previous = buildFormula(index - 1, invariant, system);
+    PTRef invariantShifted = timeMachine.sendFlaThroughTime(invariant, index - 1);
+    PTRef stepShifted = timeMachine.sendFlaThroughTime(system.getTransition(), index - 1);
+    PTRef initShifted = timeMachine.sendFlaThroughTime(system.getInit(), index);
+    return logic.mkOr(initShifted, logic.mkAnd({previous, invariantShifted, stepShifted}));
+}
+} // namespace
+
+/**
+ * Computes 1-inductive invariant from a k-inductive one using only interpolation.
+ * The idea is an application of the more general concept of reinforced unfold tranformation for CHCs from the paper
+ * "Horn Clause Solvers for Program Verification", (https://link.springer.com/chapter/10.1007/978-3-319-23534-9_2).
+ * Section 4.2 of the paper proves the correctness of the transformation and hints on use we implement here.
+ * Here we use a variant that halves the \p k (rounded up) in every iteration.
+ *
+ * Consider the definition of 1-inductive invariant as a single Horn clause in NNF:
+ * init(x^1) \lor (Inv(x^0) \land step(x^0,x^1)) \implies Inv(x^1)
+ *
+ * Unfolding this definition of $Inv$ k-1 times yields a formula equivalent to the definition of k-inductive invariant.
+ * Following the approach described in the paper, we can split the formula in two parts and compute an interpolant.
+ * Conjoining the interpolant to the original invariant yields k'-inductive invariant with k' < k.
+ * Depending on how we split the formula, we can get to different k'. The smallest k' we can get to is k/2 (rounded up).
+ *
+ * @param invariant k-inductive invsariant for the transition system \p system
+ * @param k
+ * @param system
+ * @return 1-inductive invariant for the same system that is logically stronger than the k-inductive one
+ */
+PTRef KTo1Inductive::unfold(PTRef invariant, unsigned k, TransitionSystem const & system) {
+    Logic & logic = system.getLogic();
+    TimeMachine tm(logic);
+    while (k > 1) {
+        // Split k into i + j such that i >= j
+        unsigned j = k / 2;
+        unsigned i = k - j;
+        // Build the two formulas
+        PTRef ipart = buildFormula(i, invariant, system);
+        PTRef jpart = i == j ? ipart : buildFormula(j, invariant, system);
+        PTRef shifted = tm.sendFlaThroughTime(jpart, i);
+        PTRef negatedInvariant = logic.mkNot(tm.sendFlaThroughTime(invariant, k));
+        SMTSolver solver(logic, SMTSolver::WitnessProduction::ONLY_INTERPOLANTS);
+        solver.assertProp(ipart);
+        solver.assertProp(logic.mkAnd(shifted, negatedInvariant));
+        auto res = solver.check();
+        if (res != SMTSolver::Answer::UNSAT) {
+            throw std::logic_error("Error in reducing k-inductive invariant to 1-inductive: Query must be UNSAT!");
+        }
+        auto itpContext = solver.getInterpolationContext();
+        vec<PTRef> itps;
+        ipartitions_t partitions = 1;
+        itpContext->getSingleInterpolant(itps, partitions);
+        assert(itps.size() == 1);
+        PTRef itp = tm.sendFlaThroughTime(itps[0], -static_cast<int>(i));
+        invariant = TermUtils(logic).conjoin(invariant, itp);
+        assert(i < k);
+        k = i;
+    }
+    return invariant;
+}
+
+PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) {
+    // std::cout << "Reducing k-inductive invariant with k=" << k << std::endl;
+    // Timer timer;
+    PTRef res = KTo1Inductive{KTo1Inductive::Mode::UNFOLD}.kinductiveToInductive(invariant, k, system);
+    // std::cout << timer.elapsedMilliseconds() << " ms" << std::endl;
+    return res;
 }
\ No newline at end of file
diff --git a/src/TransitionSystem.h b/src/TransitionSystem.h
index 705408a2..6305f029 100644
--- a/src/TransitionSystem.h
+++ b/src/TransitionSystem.h
@@ -82,7 +82,19 @@ class TransitionSystem {
     PTRef toNextStateVar(PTRef var) const;
 };
 
-PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem const & system);
+struct KTo1Inductive {
+    enum class Mode { UNFOLD, LEGACY };
+    explicit KTo1Inductive(Mode mode) : mode(mode) {}
+    [[nodiscard]] PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) const;
+private:
+    Mode mode;
+
+    [[nodiscard]] static PTRef legacy(PTRef invariant, unsigned k, TransitionSystem const & system);
+    [[nodiscard]] static PTRef unfold(PTRef invariant, unsigned k, TransitionSystem const & system);
+
+};
+
+PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system);