Fix error preventing postConditions from being z3ified in FairZ3Solver

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)

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 : _*))