Propagate IntInduction's precondition

src/main/scala/leon/synthesis/Heuristics.scala

@@ -55,7 +55,13 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
               , LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
             )
 
-            Solution(BooleanLiteral(true), LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
+            val pre =
+              subst( inductOn -> Variable(origId),
+                    Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)),      base.pre),
+                           And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
+                           And(LessThan(Variable(inductOn), IntLiteral(0)),    lt.pre))))
+
+            Solution(pre, LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
           case _ =>
             Solution.none
         }

src/main/scala/leon/synthesis/Task.scala

@@ -80,8 +80,8 @@ class Task(synth: Synthesizer,
         parent.partlySolvedBy(this, solution)
 
         val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
-        println(prefix+"Got: "+problem)
-        println(prefix+"Solved with: "+solution)
+        synth.reporter.info(prefix+"Got: "+problem)
+        synth.reporter.info(prefix+"Solved with: "+solution)
         Nil
 
       case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
@@ -96,10 +96,10 @@ class Task(synth: Synthesizer,
         val simplestSolution = onSuccess(simplestSubSolutions)
         minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
         val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
-        println(prefix+"Got: "+problem)
-        println(prefix+"Decomposed into:")
+        synth.reporter.info(prefix+"Got: "+problem)
+        synth.reporter.info(prefix+"Decomposed into:")
         for(p <- subProblems) {
-          println(prefix+" - "+p)
+          synth.reporter.info(prefix+" - "+p)
         }
 
         subProblems