Simplify tests

src/test/scala/leon/regression/synthesis/SynthesisSuite.scala

@@ -82,9 +82,9 @@ class SynthesisSuite extends LeonRegressionSuite {
 
   }
 
-  def forProgram(title: String, opts: Seq[LeonOption[Any]] = Nil)(content: String)(strats: PartialFunction[String, SynStrat]) {
+  def forProgram(title: String, opts: Seq[String] = Nil)(content: String)(strats: PartialFunction[String, SynStrat]) {
       test(f"Synthesizing ${nextInt()}%3d: [$title]") {
-        val ctx = testContext.copy(options = opts ++ testContext.options)
+        val ctx = createLeonContext(opts: _*)
 
         val pipeline = leon.utils.TemporaryInputPhase andThen
                        leon.frontends.scalac.ExtractionPhase andThen
@@ -118,7 +118,7 @@ class SynthesisSuite extends LeonRegressionSuite {
       }
   }
 
-  forProgram("Ground Enum", Seq(LeonOption(SharedOptions.optSelectedSolvers)(Set("enum"))))(
+  forProgram("Ground Enum", Seq("--solvers=enum"))(
     """
 import leon.annotation._
 import leon.lang._

src/test/scala/leon/regression/termination/TerminationSuite.scala

@@ -22,7 +22,7 @@ class TerminationSuite extends LeonRegressionSuite {
     new leon.utils.PreprocessingPhase     andThen
     leon.termination.TerminationPhase
 
-  private def mkTest(file : File, leonOptions: Seq[LeonOption[Any]], forError: Boolean)(block: Output=>Unit) = {
+  private def mkTest(file : File, leonOptions: Seq[String], forError: Boolean)(block: Output=>Unit) = {
     val fullName = file.getPath
     val start = fullName.indexOf("regression")
 
@@ -38,7 +38,7 @@ class TerminationSuite extends LeonRegressionSuite {
       "verification/purescala/valid/InductiveQuantification.scala"
     )
 
-    val t = if (ignored.exists(displayName endsWith _)) {
+    val t = if (ignored.exists(displayName.endsWith)) {
       ignore _
     } else {
       test _
@@ -48,10 +48,7 @@ class TerminationSuite extends LeonRegressionSuite {
       assert(file.exists && file.isFile && file.canRead,
              s"Benchmark $displayName is not a readable file")
 
-      val ctx = testContext.copy(
-        options = leonOptions,
-        files = List(file)
-      )
+      val ctx = createLeonContext((leonOptions ++ List(file.getAbsolutePath)): _* )
 
       val pipeline = mkPipeline
 

src/test/scala/leon/test/LeonRegressionSuite.scala

@@ -6,14 +6,12 @@ import leon._
 import leon.utils._
 
 import org.scalatest._
-import org.scalatest.time.Span
 import org.scalatest.concurrent._
-import org.scalatest.time.SpanSugar._
 import org.scalatest.exceptions.TestFailedException
 
 import java.io.File
 
-trait LeonRegressionSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
+trait LeonRegressionSuite extends FunSuite with Timeouts {
 
   val regressionTestDirectory = "src/test/resources"
 
@@ -23,47 +21,23 @@ trait LeonRegressionSuite extends FunSuite with Timeouts with BeforeAndAfterEach
     Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter))
   }
 
-  var testContext: LeonContext = null
-
-  override def beforeEach() = {
-    testContext = createLeonContext()
-    super.beforeEach()
-  }
-
   def testIdentifier(name: String): String = {
     def sanitize(s: String) = s.replaceAll("[^0-9a-zA-Z-]", "")
 
     sanitize(this.getClass.getName)+"/"+sanitize(name)
   }
 
-  override implicit val defaultInterruptor = new Interruptor {
-    def apply(t: Thread) {
-      testContext.interruptManager.interrupt()
-    }
-  }
-
-  def testWithTimeout(name: String, timeout: Span)(body: => Unit) {
+  override def test(name: String, tags: Tag*)(body: => Unit) {
     super.test(name) {
-      failAfter(timeout) {
-        try {
-          body
-        } catch {
-          case fe: LeonFatalError =>
-            testContext.reporter match {
-              case sr: TestSilentReporter =>
-                sr.lastErrors ++= fe.msg
-                throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
-            }
-        }
+      try {
+        body
+      } catch {
+        case fe: LeonFatalError =>
+          throw new TestFailedException("", fe, 5)
       }
     }
   }
 
-
-  override def test(name: String, tags: Tag*)(body: => Unit) {
-    testWithTimeout(name, 5.minutes)(body)
-  }
-
   protected val all : String=>Boolean = (s : String) => true
   
   def scanFilesIn(f: File, filter: String=>Boolean = all, recursive: Boolean = false): Iterable[File] = {