From 5945b7260b16f48ac810794acb2a82bc450d2afc Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 19 Dec 2012 16:34:20 +0100
Subject: [PATCH] Bugfix in Cegis.

Introducing previous counter-examples in the CEGIS loop used to produce
contradictions, because some variables were not properly freshened.
---
 src/main/scala/leon/synthesis/rules/Cegis.scala | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index cfa39a2d6..c2ab7c253 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -103,7 +103,9 @@ case object CEGIS extends Rule("CEGIS", 150) {
         }
 
         program  = And(program :: newClauses)
+
         mappings = mappings ++ newMappings
+
         recTerms = newRecTerms
 
         (newClauses, newRecTerms.keySet)
@@ -111,7 +113,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
 
       def bounds = recTerms.keySet.map(id => Not(Variable(id))).toList
       def bss = mappings.keySet
-      def css = mappings.values.map(_._1)
+      def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ recTerms.flatMap(_._2)
 
       def entireFormula = And(pathcond :: phi :: program :: bounds)
     }
@@ -228,12 +230,12 @@ case object CEGIS extends Rule("CEGIS", 150) {
                             case id if invalidModel contains id => id -> invalidModel(id)
                           }
 
-                          val counterexemple = substAll(freshCss ++ ceIn, And(Seq(unrolling.program, unrolling.phi)))
+                          val counterexample = substAll(freshCss ++ ceIn, And(Seq(unrolling.program, unrolling.phi)))
 
-                          solver1.assertCnstr(counterexemple)
-                          solver2.assertCnstr(counterexemple)
+                          solver1.assertCnstr(counterexample)
+                          solver2.assertCnstr(counterexample)
 
-                          //predicates = Not(And(unsatCore.toSeq)) +: counterexemple +: predicates
+                          //predicates = Not(And(unsatCore.toSeq)) +: counterexample +: predicates
                           solver1.assertCnstr(Not(And(unsatCore.toSeq)))
                           solver2.assertCnstr(Not(And(unsatCore.toSeq)))
                         }
-- 
GitLab