diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 2fe39ac45c0e29758684078f106bb3077fffae58..f9fe677fd88f1eb1ae1d1f71e50a4647a6781743 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -19,6 +19,9 @@ import purescala.Types._
import scala.collection.mutable.{Map => MutableMap}
+case class UnsoundExtractionException(ast: Z3AST, msg: String)
+ extends Exception("Can't extract " + ast + " : " + msg)
+
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
trait AbstractZ3Solver extends Solver {
@@ -34,6 +37,9 @@ trait AbstractZ3Solver extends Solver {
private[this] var freed = false
val traceE = new Exception()
+ protected def unsound(ast: Z3AST, msg: String): Nothing =
+ throw UnsoundExtractionException(ast, msg)
+
override def finalize() {
if (!freed) {
println("!! Solver "+this.getClass.getName+"["+this.hashCode+"] not freed properly prior to GC:")
@@ -569,9 +575,7 @@ trait AbstractZ3Solver extends Solver {
case other =>
unsupported(other, "Unexpected target type for BV value")
}
- case None => {
- throw LeonFatalError(s"Could not translate hexadecimal Z3 numeral $t")
- }
+ case None => unsound(t, "could not translate hexadecimal Z3 numeral")
}
} else {
InfiniteIntegerLiteral(v)
@@ -583,12 +587,9 @@ trait AbstractZ3Solver extends Solver {
tpe match {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
- case _ =>
- throw LeonFatalError("Unexpected target type for BV value: " + tpe.asString)
+ case _ => unsound(t, "unexpected target type for BV value: " + tpe.asString)
}
- case None => {
- throw LeonFatalError(s"Could not translate Z3NumeralIntAST numeral $t")
- }
+ case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
}
}
case Z3NumeralRealAST(n: BigInt, d: BigInt) => FractionalLiteral(n, d)
@@ -626,12 +627,12 @@ trait AbstractZ3Solver extends Solver {
val entries = elems.map {
case (IntLiteral(i), v) => i -> v
- case _ => throw LeonFatalError("Translation from Z3 to Array failed")
+ case (e,_) => unsupported(e, s"Z3 returned unexpected array index ${e.asString}")
}
finiteArray(entries, Some(default, s), to)
- case _ =>
- throw LeonFatalError("Translation from Z3 to Array failed")
+ case (s : IntLiteral, arr) => unsound(args(1), "invalid array type")
+ case (size, _) => unsound(args(0), "invalid array size")
}
}
} else {
@@ -645,7 +646,7 @@ trait AbstractZ3Solver extends Solver {
}
RawArrayValue(from, entries, default)
- case None => throw LeonFatalError("Translation from Z3 to Array failed")
+ case None => unsound(t, "invalid array AST")
}
case tp: TypeParameter =>
@@ -679,7 +680,7 @@ trait AbstractZ3Solver extends Solver {
case tpe @ SetType(dt) =>
model.getSetValue(t) match {
- case None => throw LeonFatalError("Translation from Z3 to set failed")
+ case None => unsound(t, "invalid set AST")
case Some(set) =>
val elems = set.map(e => rec(e, dt))
FiniteSet(elems, dt)
@@ -709,8 +710,7 @@ trait AbstractZ3Solver extends Solver {
// case OpDiv => Division(rargs(0), rargs(1))
// case OpIDiv => Division(rargs(0), rargs(1))
// case OpMod => Modulo(rargs(0), rargs(1))
- case other =>
- throw LeonFatalError(
+ case other => unsound(t,
s"""|Don't know what to do with this declKind: $other
|Expected type: ${Option(tpe).map{_.asString}.getOrElse("")}
|Tree: $t
@@ -719,8 +719,7 @@ trait AbstractZ3Solver extends Solver {
}
}
}
- case _ =>
- throw LeonFatalError(s"Don't know what to do with this Z3 tree: $t")
+ case _ => unsound(t, "unexpected AST")
}
}
rec(tree, tpe)
@@ -731,6 +730,8 @@ trait AbstractZ3Solver extends Solver {
Some(fromZ3Formula(model, tree, tpe))
} catch {
case e: Unsupported => None
+ case e: UnsoundExtractionException => None
+ case n: java.lang.NumberFormatException => None
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index a187549c514cc8fc83ec7476493e1d9e96a48763..c129243d15b661d9e42d578447fdea6cb1aea3e0 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -65,26 +65,14 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
val optEnabler = model.evalAs[Boolean](b)
if (optEnabler == Some(true)) {
- // FIXME: Dirty hack!
- // Unfortunately, blockers don't lead to a true decision tree where all
- // unexecutable branches are false since we have
- // b1 ==> ( b2 \/ b3)
- // b1 ==> (!b2 \/ !b3)
- // so b2 /\ b3 is possible when b1 is false. This leads to unsound models
- // (like Nil.tail) which obviously cannot be part of a domain but can't be
- // translated back from Z3 either.
- try {
- val optArgs = (m.args zip fromTypes).map {
- p => softFromZ3Formula(model, model.eval(Matcher.argValue(p._1), true).get, p._2)
- }
+ val optArgs = (m.args zip fromTypes).map {
+ p => softFromZ3Formula(model, model.eval(Matcher.argValue(p._1), true).get, p._2)
+ }
- if (optArgs.forall(_.isDefined)) {
- Set(optArgs.map(_.get))
- } else {
- Set.empty
- }
- } catch {
- case _: Throwable => Set.empty
+ if (optArgs.forall(_.isDefined)) {
+ Set(optArgs.map(_.get))
+ } else {
+ Set.empty
}
} else {
Set.empty