diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 16f1ddb88e46e492589b21c46aed55aeb129ce3f..254c6a2f5e468fc5af3b22d6b9ae4b2530f05fc9 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -2,12 +2,10 @@
 
 package leon.regression.repair
 
-import leon._
 import leon.test._
 import leon.utils._
 import leon.frontends.scalac.ExtractionPhase
 import leon.repair._
-import leon.verification.VerificationPhase
 
 class RepairSuite extends LeonRegressionSuite {
   val pipeline = ExtractionPhase andThen 
@@ -31,23 +29,12 @@ class RepairSuite extends LeonRegressionSuite {
     val path = file.getAbsoluteFile.toString
     val name = file.getName
 
-    val reporter = new TestSilentReporter
-    //val reporter = new DefaultReporter(Set(utils.DebugSectionRepair))
-
-    val ctx = new LeonContext(
-      reporter = reporter,
-      interruptManager = new InterruptManager(reporter),
-      options = Seq(
-        LeonOption(GlobalOptions.optFunctions)(Seq(fileToFun(name))),
-        LeonOption(VerificationPhase.optParallelVCs)(true),
-        LeonOption(GlobalOptions.optTimeout)(180L)
-      )
-    )
+    val ctx = createLeonContext("--parallel", "--timeout=180", "--solvers=smt-z3")
 
     test(name) {
       pipeline.run(ctx, List(path))
-      if(reporter.errorCount > 0) {
-        fail("Errors during repair:\n"+reporter.lastErrors.mkString("\n"))
+      if(ctx.reporter.errorCount > 0) {
+        fail("Errors during repair:\n"+ctx.reporter.asInstanceOf[TestSilentReporter].lastErrors.mkString("\n"))
       }
     }
   }
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index 723c8319d7290523ad0e660ee722e41f13f226f4..06abffdefb888208b7cfb7904efba5d3434eb835 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -20,7 +20,7 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
   }
 
   private def testSynthesis(cat: String, f: File, bound: Int) {
-    val ctx = createLeonContext("--synthesis")
+    val ctx = createLeonContext("--synthesis", "--solvers=smt-z3")
 
     val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase