From bd95821806b52052d58ba44b43f621c7387ae77b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 12 Feb 2014 16:29:44 +0100
Subject: [PATCH] Fix IntInduction
---
.../scala/leon/synthesis/heuristics/IntInduction.scala | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index c5773af48..9cbe13c89 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) =>
--
GitLab