diff --git a/src/cp/CallTransformation.scala b/src/cp/CallTransformation.scala
index b0a0880ec1ac1e802389e6d5549059c8af34512f..ab8a96f5829bf622f2914e0ecbae66207f614f43 100644
--- a/src/cp/CallTransformation.scala
+++ b/src/cp/CallTransformation.scala
@@ -552,7 +552,7 @@ object CallTransformation {
         case None => expr
         case Some(b) => And(expr, GreaterThan(minExpr, IntLiteral(b)))
       }
-      println("Now calling findAllMinimizing with " + toCheck)
+      // purescala.Settings.reporter.info("Now calling findAllMinimizing with " + toCheck)
       val minValue = chooseMinimizingModelAndValue(program, toCheck, outputVars, minExpr, inputConstraints)._2
 
       val minValConstraint    = And(expr, Equals(minExpr, IntLiteral(minValue)))
diff --git a/src/cp/CodeExtraction.scala b/src/cp/CodeExtraction.scala
index 4d9ab2e5fbca0b57f1df84e7b7d7eb20f4d10ea9..13253aacc51d5cfa2e6e9a4d218024dc222662f9 100644
--- a/src/cp/CodeExtraction.scala
+++ b/src/cp/CodeExtraction.scala
@@ -650,7 +650,7 @@ trait CodeExtraction extends Extractors {
           if (tolerant) {
             val varTpe = scalaType2PureScala(unit, silent)(sym.tpe)
             val newID = FreshIdentifier(sym.name.toString).setType(varTpe)
-            externalSubsts(i) = (() => Variable(newID))
+            varSubsts(sym) = (() => Variable(newID))
             Variable(newID)
           } else {
             unit.error(tr.pos, "Unidentified variable.")
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 134af47306e96ebc2dd52fbd306617e0dcf8d7c8..484d1b1010a5446752e773a171fe7bc974416495 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -177,6 +177,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   private var reverseFunctionMap: Map[Z3FuncDecl, FunDef] = Map.empty
 
   def prepareFunctions: Unit = {
+    functionMap = Map.empty
+    reverseFunctionMap = Map.empty
     for (funDef <- program.definedFunctions) {
       val sortSeq = funDef.args.map(vd => typeToSort(vd.tpe))
       val returnSort = typeToSort(funDef.returnType)