diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala index e882900023c2d72cef5bbac04c9cba0b6c045cba..9013002f8c4e853bfb5ef65b5eeeed4972033168 100644 --- a/src/test/scala/leon/test/verification/NewSolversRegression.scala +++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala @@ -32,7 +32,7 @@ class NewSolversRegression extends VerificationRegression { ( if (isZ3Available) - List(List("--solvers=smt-z3-quantified", "--feelinglucky")) + List(List("--solvers=smt-z3-quantified", "--feelinglucky", "--timeout=3")) else Nil ) ++ ( if (isCVC4Available) diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala index 2cd355a6601548914e102cfa23fc4cb686820a01..36f578b131175542513abaa70f2f86798a207e89 100644 --- a/src/test/scala/leon/test/verification/VerificationRegression.scala +++ b/src/test/scala/leon/test/verification/VerificationRegression.scala @@ -10,9 +10,6 @@ import leon.purescala.Definitions.Program import leon.frontends.scalac.ExtractionPhase import leon.utils.PreprocessingPhase -import _root_.smtlib.interpreters._ - -import java.io.File // If you add another regression test, make sure it contains one object whose name matches the file name // This is because we compile all tests from each folder separately. @@ -51,7 +48,7 @@ trait VerificationRegression extends LeonTestSuite { } } - private[verification] def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) { + private[verification] def forEachFileIn(cat : String)(block : Output=>Unit) { val fs = filesInResourceDir( testDir + cat, _.endsWith(".scala")).toList fs foreach { file =>