diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index c5773af4828c6fa6134f0599288e3d6c587b09c8..9cbe13c89c7d4159c945b1398030edba066b06f3 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -24,12 +24,13 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
         val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
 
         val newPhi     = subst(origId -> Variable(inductOn), p.phi)
+        val newPc      = subst(origId -> Variable(inductOn), p.pc)
         val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi)
         val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
 
-        val subBase = Problem(List(), p.pc, subst(origId -> IntLiteral(0), p.phi), p.xs)
-        val subGT   = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.pc)), newPhi, p.xs)
-        val subLT   = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.pc)), newPhi, p.xs)
+        val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.pc), subst(origId -> IntLiteral(0), p.phi), p.xs)
+        val subGT   = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, newPc)), newPhi, p.xs)
+        val subLT   = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, newPc)), newPhi, p.xs)
 
         val onSuccess: List[Solution] => Option[Solution] = {
           case List(base, gt, lt) =>