From 5513dab8f1bf523a7722ecea7925e05514f9f157 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 2 Feb 2016 14:00:31 +0100
Subject: [PATCH] Uniform way of detecting solvers, making sure latest versions
 of CVC4 work.

---
 .../scala/leon/solvers/SolverFactory.scala    |  4 ++--
 .../verification/NewSolversSuite.scala        | 19 ++++---------------
 .../verification/XLangVerificationSuite.scala |  9 ++-------
 .../PureScalaVerificationSuite.scala          | 17 +++--------------
 4 files changed, 11 insertions(+), 38 deletions(-)

diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 6b2d4272b..67d28f877 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 15e02a693..5a340d1f8 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 8511ebfea..0136b7b06 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 93b2a2699..6c450c1c8 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(
-- 
GitLab