From a6566fa7d2e116c7d9eb698a6f63a7cc2abe241a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 26 May 2015 15:41:41 +0200
Subject: [PATCH] Kick the new z3 solver out of tests for now
---
.../verification/NewSolversRegression.scala | 20 ++++---------------
1 file changed, 4 insertions(+), 16 deletions(-)
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
index a85ff1629..9322f2691 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
+
}
}
--
GitLab