Fixed total model extraction in QuantificationManager

epfl-lara · Apr 28, 2016 · 05ed414 · 05ed414
1 parent c64c7a8
commit 05ed414
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -1199,8 +1199,12 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
               }
             }.toMap
 
-            if (conditionals.isEmpty) {
-              value
+            if (conditionals.isEmpty) f match {
+              case FiniteLambda(mapping, dflt, tpe) =>
+                Lambda(params.map(ValDef(_)), mapping.foldRight(dflt) { case ((es, v), elze) =>
+                  IfExpr(andJoin((params zip es).map(p => Equals(p._1.toVariable, p._2))), v, elze)
+                })
+              case _ => f
             } else {
               val ((_, dflt)) +: rest = conditionals.toSeq.sortBy { case (conds, _) =>
                 (conds.flatMap(variablesOf).toSet.size, conds.size)

diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -54,6 +54,7 @@ trait AbstractZ3Solver extends Solver {
   )
 
   // @nv: This MUST take place AFTER Z3Context was created!!
+  // Well... actually maybe not, but let's just leave it here to be sure
   toggleWarningMessages(true)
 
   protected var solver : Z3Solver  = null