From a5c459d702a6648fdb578383cbacd2d84487d485 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 16 Apr 2015 18:12:33 +0200
Subject: [PATCH] Update to the new version of scala-smtlib
---
project/Build.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala | 2 +-
.../scala/leon/test/verification/NewSolversRegression.scala | 4 ++--
.../test/verification/PureScalaVerificationRegression.scala | 4 ++--
.../leon/test/verification/XLangVerificationRegression.scala | 4 ++--
6 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/project/Build.scala b/project/Build.scala
index be7d12251..284491fff 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -80,6 +80,6 @@ object Leon extends Build {
def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "3dcd7ba20e5dcddd777c57466b60f7c4d86a3ff2")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "9f88509b13e7e64214c0b9b6a9124fc6c29e2084")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 8074d9f9a..aafe81e71 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -21,7 +21,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def targetName = "cvc4"
- def getNewInterpreter() = new CVC4Interpreter
+ def getNewInterpreter() = CVC4Interpreter.buildDefault
override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 1aed748ea..a11ab2978 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -23,7 +23,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
def targetName = "z3"
- def getNewInterpreter() = new Z3Interpreter
+ def getNewInterpreter() = Z3Interpreter.buildDefault
val extSym = SSymbol("_")
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
index f73ab1a1a..236e597d6 100644
--- a/src/test/scala/leon/test/verification/NewSolversRegression.scala
+++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala
@@ -15,7 +15,7 @@ class NewSolversRegression extends VerificationRegression {
val pipeBack = AnalysisPhase
val optionVariants: List[List[String]] = {
val isZ3Available = try {
- new Z3Interpreter()
+ Z3Interpreter.buildDefault
true
} catch {
case e: java.io.IOException =>
@@ -23,7 +23,7 @@ class NewSolversRegression extends VerificationRegression {
}
val isCVC4Available = try {
- new CVC4Interpreter()
+ CVC4Interpreter.buildDefault
true
} catch {
case e: java.io.IOException =>
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 204132219..2cffcc1b3 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -16,7 +16,7 @@ class PureScalaVerificationRegression extends VerificationRegression {
val pipeBack = AnalysisPhase
val optionVariants: List[List[String]] = {
val isZ3Available = try {
- new Z3Interpreter()
+ Z3Interpreter.buildDefault
true
} catch {
case e: java.io.IOException =>
@@ -24,7 +24,7 @@ class PureScalaVerificationRegression extends VerificationRegression {
}
val isCVC4Available = try {
- new CVC4Interpreter()
+ CVC4Interpreter.buildDefault
true
} catch {
case e: java.io.IOException =>
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 425ee3c2c..6846cd693 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -64,7 +64,7 @@ class XLangVerificationRegression extends LeonTestSuite {
_.endsWith(".scala"))
val isZ3Available = try {
- new Z3Interpreter()
+ Z3Interpreter.buildDefault
true
} catch {
case e: java.io.IOException =>
@@ -72,7 +72,7 @@ class XLangVerificationRegression extends LeonTestSuite {
}
val isCVC4Available = try {
- new CVC4Interpreter()
+ CVC4Interpreter.buildDefault
// @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
true
} catch {
--
GitLab