diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 89cfe4492b914c630e5122993700f4945f1662b5..e9fdde89c3555b41b47b696c542733b0bf411830 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -99,7 +99,7 @@ object Extensions {
 
     allLoaded = defaultExtensions ++ loaded
     analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
-    analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
+    //analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
 
     val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
     val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 10ab5ef7b5bf3c296b5bf79288987d076d26f94c..0ca94eb2d9a484f385bb5d35e20ae71c6d436855 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -13,8 +13,10 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
   def description: String = "Generate random testcases"
   override def shortDescription: String = "test"
 
+  private val z3Solver = new FairZ3Solver(reporter)
 
   def analyse(program: Program) {
+    z3Solver.setProgram(program)
     reporter.info("Running test generation")
     val allFuns = program.definedFunctions
     allFuns.foreach(fd => {
@@ -37,7 +39,7 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
       reporter.info("Now considering path condition: " + pathCond)
 
       var testcase: Option[Map[Identifier, Expr]] = None
-      val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
+      //val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
         
       z3Solver.init()
       z3Solver.restartZ3