Attach preconditions

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

@@ -46,7 +46,15 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
 
         val onSuccess: List[Solution] => Solution = {
           case List(base, gt, lt) =>
+            val preIn = 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)))
+            val preOut = subst(inductOn -> Variable(origId), preIn)
+
             val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
+
+            newFun.precondition = Some(preIn)
+
             newFun.body = Some(
               IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
                 base.toExpr,
@@ -55,13 +63,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
               , LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
             )
 
-            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)))))
+            Solution(preOut, LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
           case _ =>
             Solution.none
         }