Removed caught LeonFatalErrors from AbstractZ3Solver

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,7 @@ trait AbstractZ3Solver extends Solver {
       Some(fromZ3Formula(model, tree, tpe))
     } catch {
       case e: Unsupported => None
+      case e: UnsoundExtractionException => None
     }
   }
 

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