diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala index 6b2d4272b37b4a06ba2731c5049bcc043b87c927..67d28f877019a3e4741df6d268c68fc2d86d17ee 100644 --- a/src/main/scala/leon/solvers/SolverFactory.scala +++ b/src/main/scala/leon/solvers/SolverFactory.scala @@ -177,7 +177,7 @@ object SolverFactory { } lazy val hasZ3 = try { - Z3Interpreter.buildDefault.free() + new Z3Interpreter("z3", Array("-in", "-smt2")) true } catch { case e: java.io.IOException => @@ -185,7 +185,7 @@ object SolverFactory { } lazy val hasCVC4 = try { - CVC4Interpreter.buildDefault.free() + new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5")) true } catch { case e: java.io.IOException => diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala index 15e02a693988e44be555c5e954be65cab4203086..5a340d1f870e019f33460fb6e386c50e58fbcbff 100644 --- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala +++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala @@ -5,6 +5,7 @@ package leon.regression.verification import _root_.smtlib.interpreters._ import leon._ import leon.verification.VerificationPhase +import leon.solvers.SolverFactory /* @EK: Disabled for now as many tests fail class NewSolversSuite extends VerificationSuite { @@ -14,21 +15,9 @@ class NewSolversSuite extends VerificationSuite { val pipeBack = AnalysisPhase val optionVariants: List[List[String]] = { - val isCVC4Available = try { - CVC4Interpreter.buildDefault.free() - true - } catch { - case e: java.io.IOException => - false - } - - val isZ3Available = try { - Z3Interpreter.buildDefault.free() - true - } catch { - case e: java.io.IOException => - false - } + val isCVC4Available = SolverFactory.hasCVC4 + + val isZ3Available = SolverFactory.hasZ3 ( if (isCVC4Available) diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala index 8511ebfea95d4d6a412d82922ffb1e6fb870d312..0136b7b06643985265c738e39402e6a3d3d33f99 100644 --- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala @@ -3,19 +3,14 @@ package leon.regression.verification import smtlib.interpreters.Z3Interpreter +import leon.solvers.SolverFactory // If you add another regression test, make sure it contains exactly one object, whose name matches the file name. // This is because we compile all tests from each folder together. class XLangVerificationSuite extends VerificationSuite { val optionVariants: List[List[String]] = { - val isZ3Available = try { - Z3Interpreter.buildDefault.free() - true - } catch { - case e: java.io.IOException => - false - } + val isZ3Available = SolverFactory.hasZ3 List( List(), diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala index 93b2a2699c7894737056e5c7fa969cebdcfe255f..6c450c1c8613f74c5a6679aaaf6035f59e593e66 100644 --- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala @@ -4,6 +4,7 @@ package leon.regression.verification package purescala import smtlib.interpreters.{CVC4Interpreter, Z3Interpreter} +import leon.solvers.SolverFactory // 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 together. @@ -11,21 +12,9 @@ abstract class PureScalaVerificationSuite extends VerificationSuite { val testDir = "regression/verification/purescala/" - val isZ3Available = try { - new Z3Interpreter("z3", Array("-in", "-smt2")) - true - } catch { - case e: java.io.IOException => - false - } + val isZ3Available = SolverFactory.hasZ3 - val isCVC4Available = try { - new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5")) - true - } catch { - case e: java.io.IOException => - false - } + val isCVC4Available = SolverFactory.hasCVC4 val opts: List[List[String]] = { List(