From 83139845a8024f5d1241e53e1bfdf4db20aa6037 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 28 Oct 2016 13:46:59 +0200
Subject: [PATCH] Fix for model extraction in UnrollingSolver
---
.../inox/solvers/unrolling/QuantificationTemplates.scala | 2 +-
src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala | 5 +++--
src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala | 2 +-
3 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 4cd8f09a2..8c1358805 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -909,7 +909,7 @@ trait QuantificationTemplates { self: Templates =>
clauses += mkSubstituter(substMap)(mkImplies(b, clause))
}
- for (q <- quantifications) {
+ for (q <- quantifications if ignoredSubsts.isDefinedAt(q)) {
val guard = Variable(FreshIdentifier("guard", true), BooleanType)
val elems = q.quantifiers.map(_._1)
val values = elems.map(v => v.freshen)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 08f296e02..915aa9edb 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -385,9 +385,10 @@ trait AbstractUnrollingSolver extends Solver { self =>
p => (unflatten(p._1) zip unflatten(p._2)).map(p => (p._1, andJoin(p._2.flatten)))
}
- val default = extractValue(unflatten(flatArguments.last._1).foldLeft(f -> (tpe: Type)) {
+ val (app, to) = unflatten(flatArguments.last._1).foldLeft(f -> (tpe: Type)) {
case ((f, tpe: FunctionType), args) => (templates.mkApp(f, encode(tpe), args), tpe.to)
- }._1, tpe)
+ }
+ val default = extractValue(app, to)
extract(f, tpe, params, allArguments, default)._1
}
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index fd394dfb8..59a16643c 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -503,7 +503,7 @@ trait AbstractZ3Solver
kind match {
case Z3NumeralIntAST(Some(v)) =>
val leading = t.toString.substring(0, 2 min t.toString.length)
- if(leading == "#x") {
+ if (leading == "#x") {
_root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
case Some(hexa) =>
tpe match {
--
GitLab