From 9bdbf0e3382c54591d60464d136f3b7509826b6c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 14 Nov 2012 22:00:40 +0100
Subject: [PATCH] Fix shape of postconditions
---
src/main/scala/leon/synthesis/Heuristics.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index b89735441..4f51d8c05 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -73,7 +73,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
newFun.precondition = Some(preIn)
- newFun.postcondition = Some(And(Equals(ResultVariable(), Tuple(p.xs.map(Variable(_)))), p.phi))
+ newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable(), p.phi))
newFun.body = Some(
IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
@@ -248,7 +248,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
val outerPre = Or(globalPre)
newFun.precondition = Some(funPre)
- newFun.postcondition = Some(And(Equals(ResultVariable(), Tuple(p.xs.map(Variable(_)))), p.phi))
+ newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable(), p.phi))
newFun.body = Some(MatchExpr(Variable(inductOn), cases))
--
GitLab