Skip to content
Snippets Groups Projects
Commit c0625343 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Add timeouts to all regression suites

parent b8491c85
No related branches found
No related tags found
No related merge requests found
...@@ -19,7 +19,7 @@ class OrbRegressionSuite extends LeonRegressionSuite { ...@@ -19,7 +19,7 @@ class OrbRegressionSuite extends LeonRegressionSuite {
} }
private def testInference(f: File, bound: Option[Int] = None) { 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 val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil) val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
......
...@@ -76,7 +76,7 @@ class StablePrintingSuite extends LeonRegressionSuite { ...@@ -76,7 +76,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
while(workList.nonEmpty) { while(workList.nonEmpty) {
val reporter = new TestSilentReporter val reporter = new TestSilentReporter
val ctx = createLeonContext("--synthesis").copy(reporter = reporter) val ctx = createLeonContext("--synthesis", "--timeout=120").copy(reporter = reporter)
val j = workList.pop() val j = workList.pop()
info(j.info("compilation")) info(j.info("compilation"))
......
...@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite { ...@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) { private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
for(f <- files) { for(f <- files) {
mkTest(f, Seq("--solvers=smt-z3"), forError)(block) mkTest(f, Seq("--solvers=smt-z3", "--timeout=120"), forError)(block)
} }
} }
......
...@@ -12,14 +12,14 @@ class XLangVerificationSuite extends VerificationSuite { ...@@ -12,14 +12,14 @@ class XLangVerificationSuite extends VerificationSuite {
val optionVariants: List[List[String]] = { val optionVariants: List[List[String]] = {
val isZ3Available = SolverFactory.hasZ3 val isZ3Available = SolverFactory.hasZ3
List( (List(
List(), List(),
List("--feelinglucky") List("--feelinglucky")
) ++ ( ) ++ (
if (isZ3Available) if (isZ3Available)
List(List("--solvers=smt-z3", "--feelinglucky")) List(List("--solvers=smt-z3", "--feelinglucky"))
else Nil else Nil
) )).map ("--timeout=120" :: _)
} }
val testDir: String = "regression/verification/xlang/" val testDir: String = "regression/verification/xlang/"
......
...@@ -14,7 +14,7 @@ class XLangDesugaringSuite extends LeonRegressionSuite { ...@@ -14,7 +14,7 @@ class XLangDesugaringSuite extends LeonRegressionSuite {
def testFrontend(f: File, forError: Boolean) = { def testFrontend(f: File, forError: Boolean) = {
test ("Testing " + f.getName) { test ("Testing " + f.getName) {
val ctx = createLeonContext() val ctx = createLeonContext("--timeout=40")
if (forError) { if (forError) {
intercept[LeonFatalError]{ intercept[LeonFatalError]{
pipeline.run(ctx, List(f.getAbsolutePath)) pipeline.run(ctx, List(f.getAbsolutePath))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment