diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index aae1dcc84f2375e56ef0ed65dbf92be3a24dc297..99349648434acb1047ac31d6328a16bd865a5d77 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -122,36 +122,16 @@ trait AbstractZ3Solver {
       neverInitialized = false
       z3 = new Z3Context(z3cfg)
       solver = z3.mkSolver
+      prepareSorts
+      prepareFunctions
     } else {
       solver = z3.mkSolver
     }
 
     exprToZ3Id = Map.empty
     z3IdToExpr = Map.empty
-
-    fallbackSorts = Map.empty
-
-    mapSorts = Map.empty
-    arraySorts = Map.empty
-    funSorts = Map.empty
-    funDomainConstructors = Map.empty
-    funDomainSelectors = Map.empty
-
-    tupleSorts = Map.empty
-    tupleConstructors = Map.empty
-    tupleSelectors = Map.empty
-
-    mapRangeSorts.clear
-    mapRangeSomeConstructors.clear
-    mapRangeNoneConstructors.clear
-    mapRangeSomeTesters.clear
-    mapRangeNoneTesters.clear
-    mapRangeValueSelectors.clear
-
-    prepareSorts
-
-    prepareFunctions
   }
+
   protected[leon] def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
     case Some(z3sort) => z3sort
     case None => {
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 4001d53450e6c6b4d12751aaacbd3b18f0ccfc98..93c0e8e737940685eb043b2974cee965da38b29e 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -306,7 +306,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
           // reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message)
           reporter.warning("Z3 doesn't know because ??")
           foundAnswer(None)
-          m.delete
         }
         case (Some(true), m) => { // SAT
           validatingStopwatch.start
@@ -336,8 +335,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
         // This branch is both for with and without unsat cores. The
         // distinction is made inside.
         case (Some(false), m) => {
-          //m.delete
-
           if(!Settings.useCores)
             solver.pop(1)
             
@@ -540,7 +537,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
       }).toMap
 
       val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
-      model.delete
       lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
       val evalResult = eval(asMap, formula, evaluator)
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 08b27c9ed72f54fcbab108f3c25644280c95a8e7..9215e6c40aceaf9e273265e5370b5058c7794880 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -61,17 +61,17 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with
     val unsatResult   = (Some(false), emptyModel)
 
     val result = toZ3Formula(expression).map { asZ3 => 
-      z3.assertCnstr(asZ3)
-      z3.checkAndGetModel() match {
-        case (Some(false), _) => unsatResult
-        case (Some(true), model) => {
+      solver.assertCnstr(asZ3)
+      solver.check match {
+        case Some(false) => unsatResult
+        case Some(true) => {
+          val model = solver.getModel
+
           if(containsFunctionCalls(expression)) {
             unknownResult
           } else { 
             val variables = variablesOf(expression)
-            val r = (Some(true), modelToMap(model, variables))
-            model.delete
-            r
+            (Some(true), modelToMap(model, variables))
           }
         }
         case _ => unknownResult
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index 184714e7b2b90fd9e220c75324fbc96479590175..9d24d1d27ca966640d313bd805e9d793ed31dd5a 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -14,7 +14,7 @@ class ParallelSearch(synth: Synthesizer,
 
   def initWorkerContext(wr: ActorRef) = {
     val reporter = new SilentReporter
-    val solver = new FairZ3Solver(synth.context)
+    val solver = new FairZ3Solver(synth.context.copy(reporter = reporter))
     solver.setProgram(synth.program)
 
     SynthesisContext(solver = solver, reporter = synth.reporter)