Fix for model extraction in UnrollingSolver

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)

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
         }

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 {