diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala index 5bc2255dbebb4b2c4f652c52627d94479e18c51a..a8d4113f3cc6d2dbd1129a730a0636ac76912e50 100644 --- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala +++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala @@ -19,7 +19,7 @@ class OrbRegressionSuite extends LeonRegressionSuite { } private def testInference(f: File, bound: Option[Int] = None) { - val ctx = createLeonContext("--inferInv", "--vcTimeout=3", "--solvers=smt-z3", "--silent") + val ctx = createLeonContext("--inferInv", "--vcTimeout=3", "--solvers=smt-z3", "--silent", "--timeout=120") val beginPipe = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil) diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala index 6ab235dd5dda3f1c9e087ca0c93b374f07dec5df..346a6057d5c265a8a9127f765d67cc5843d29c5a 100644 --- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala +++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala @@ -76,7 +76,7 @@ class StablePrintingSuite extends LeonRegressionSuite { while(workList.nonEmpty) { val reporter = new TestSilentReporter - val ctx = createLeonContext("--synthesis").copy(reporter = reporter) + val ctx = createLeonContext("--synthesis", "--timeout=120").copy(reporter = reporter) val j = workList.pop() info(j.info("compilation")) diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala index 876ad77bde182b5fd380300a69b3963929eaee31..94a31ac66f7cbcbf70e4acf9607b6f3e489699e3 100644 --- a/src/test/scala/leon/regression/termination/TerminationSuite.scala +++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala @@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite { private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) { for(f <- files) { - mkTest(f, Seq("--solvers=smt-z3"), forError)(block) + mkTest(f, Seq("--solvers=smt-z3", "--timeout=120"), forError)(block) } } diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala index efecaf71a5b027bbd88813d5a88971fa3f0184eb..a49cf4d3fbdf0e8bb1ad1a00d1660ce8f8d7c52f 100644 --- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala @@ -12,14 +12,14 @@ class XLangVerificationSuite extends VerificationSuite { val optionVariants: List[List[String]] = { val isZ3Available = SolverFactory.hasZ3 - List( + (List( List(), List("--feelinglucky") ) ++ ( if (isZ3Available) List(List("--solvers=smt-z3", "--feelinglucky")) else Nil - ) + )).map ("--timeout=120" :: _) } val testDir: String = "regression/verification/xlang/" diff --git a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala index 9625953a9f886bca89c5de4b2972d489f66e50f6..4781e6a88af5f227394bf2b539b3e7d52cd27d66 100644 --- a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala +++ b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala @@ -14,7 +14,7 @@ class XLangDesugaringSuite extends LeonRegressionSuite { def testFrontend(f: File, forError: Boolean) = { test ("Testing " + f.getName) { - val ctx = createLeonContext() + val ctx = createLeonContext("--timeout=40") if (forError) { intercept[LeonFatalError]{ pipeline.run(ctx, List(f.getAbsolutePath))