diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala index f75e44e6dc7cf9eac4f39d22fff0dff121e89e59..28cb94845a8174413b4bb099449d47bb0a67aef5 100644 --- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala +++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala @@ -26,8 +26,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50) val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi) val subBase = Problem(List(), p.c, subst(origId -> IntLiteral(0), p.phi), p.xs) - val subGT = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs) - val subLT = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs) + val subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.c)), newPhi, p.xs) + val subLT = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.c)), newPhi, p.xs) val onSuccess: List[Solution] => Solution = { case List(base, gt, lt) => diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala index ac005a3803fa02b6e0992e7c1dd1b296e8b6a509..8225c7b6ca2ca3c9151b61309d14d5b1ec8b96af 100644 --- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala +++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala @@ -22,7 +22,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn var predicates: Seq[Expr] = Seq() while (result.isEmpty && i < maxTries) { - val phi = And(p.phi +: predicates) + val phi = And(p.c +: p.phi +: predicates) //println("SOLVING " + phi + " ...") synth.solver.solveSAT(phi) match { case (Some(true), satModel) =>