From c06253438e72249f4023642898bb7842a09893b2 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 14:36:35 +0200
Subject: [PATCH] Add timeouts to all regression suites
---
src/test/scala/leon/regression/orb/OrbRegressionSuite.scala | 2 +-
.../scala/leon/regression/synthesis/StablePrintingSuite.scala | 2 +-
.../scala/leon/regression/termination/TerminationSuite.scala | 2 +-
.../leon/regression/verification/XLangVerificationSuite.scala | 4 ++--
.../scala/leon/regression/xlang/XLangDesugaringSuite.scala | 2 +-
5 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 5bc2255db..a8d4113f3 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 6ab235dd5..346a6057d 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 876ad77bd..94a31ac66 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 efecaf71a..a49cf4d3f 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 9625953a9..4781e6a88 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))
--
GitLab