diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index d836e5f9e8ffdb5133b067a135b6c25cba34be7e..aefe9fd2c89a8d4728e2f85282a68e93b6bd6adc 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -393,7 +393,7 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
             //   scala.sys.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
             // }
 
-            assert(!this.isInstanceOf[FairZ3Solver], "This should not happen using FairZ3Solver")
+            assert(!this.isInstanceOf[FairZ3Solver], "Trying to convert unknown variable '"+id+"' while using FairZ3")
 
             val newAST = z3.mkFreshConst(id.uniqueName/*name*/, typeToSort(v.getType))
             z3Vars = z3Vars + (id -> newAST)
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 5e4d08d0e9add649a3ebac937c24ac87446fbd22..6a4a96e1519d01077bfcecca0664702ef9da524f 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -205,7 +205,7 @@ object FunctionTemplate {
         }
 
       val finalPred2 : Expr = rec(activatingBool, true, postHolds)
-      storeGuarded(activatingBool, true, postHolds)
+      storeGuarded(activatingBool, true, finalPred2)
     }
 
     new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*))