From 43c45c32d8fa5cd5cab6174ff46e6807ad88d60d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 12 May 2016 12:39:00 +0200
Subject: [PATCH] Fix bug in CEGIS
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index bc552f06f..e572ab185 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -448,14 +448,15 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
val innerSol = outerExprToInnerExpr(outerSol)
val cnstr = letTuple(p.xs, innerSol, innerPhi)
- cTreeFd.fullBody = innerSol
-
- timers.testForProgram.start()
def withBindings(e: Expr) = p.pc.bindings.foldRight(e){
case ((id, v), bd) => let(id, outerExprToInnerExpr(v), bd)
}
+ cTreeFd.fullBody = withBindings(innerSol) // FIXME! This shouldnt be needed... Solution around should be somehow used
+
+ timers.testForProgram.start()
+
val boundCnstr = withBindings(cnstr)
val res = ex match {
@@ -482,6 +483,8 @@ abstract class CEGISLike(name: String) extends Rule(name) {
case EvaluationResults.EvaluatorError(err) =>
debug("Error testing CE: "+err)
+ //println(s"InnerSol: $innerSol")
+ //println(s"Constr : $boundCnstr")
None
}
--
GitLab