diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 4cd8f09a2ef1ae751702ea8f764539191b491e02..8c135880502a438204336f277cea58c895144c1d 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 08f296e023f718b4c1456bf5d80cf072037c3a62..915aa9edbd74f6eb8284b9a7d85ac827a4a26ef0 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 fd394dfb8317d4c33836ac6a280a8cdb936d06d3..59a16643caa53e61406ed2a4fca3ec020a1cb0f2 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 {