diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala index a85ff1629271c9e4ac866e68c31b681419de2cee..9322f269176dd2933717249a5a1df79b0cbca6b0 100644 --- a/src/test/scala/leon/test/verification/NewSolversRegression.scala +++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala @@ -16,13 +16,6 @@ class NewSolversRegression extends VerificationRegression { val pipeFront = xlang.NoXLangFeaturesChecking val pipeBack = AnalysisPhase val optionVariants: List[List[String]] = { - val isZ3Available = try { - Z3Interpreter.buildDefault - true - } catch { - case e: java.io.IOException => - false - } val isCVC4Available = try { CVC4Interpreter.buildDefault @@ -32,14 +25,9 @@ class NewSolversRegression extends VerificationRegression { false } - ( - if (isZ3Available) - List(List("--solvers=smt-z3-q", "--feelinglucky", "--timeout=3")) - else Nil - ) ++ ( - if (isCVC4Available) - List(List("--solvers=smt-cvc4-proof", "--feelinglucky", "--timeout=3")) - else Nil - ) + if (isCVC4Available) + List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof", "--timeout=15")) + else Nil + } }