diff --git a/project/Build.scala b/project/Build.scala
index be7d12251bcb4a0402b89dd10fe1a8599593defa..284491fff92a1fb8348dd81874099ff4be7019fe 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 8074d9f9a02fa7cc33d6acb6b551b6ae222a22b0..aafe81e718b4bd18692c9d0ef3154d96921244ff 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 1aed748ea0cdbd5e314267656477faa6c68bdb75..a11ab2978305c1e0c6c04732a2b3e2edd5f1ef0d 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 f73ab1a1ab352653d2631b02ce73ff30015ee5f7..236e597d6aebaa44c10e0e83421d9816f284ff87 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 2041322191909b59e49fd4aca0c061de492fdec8..2cffcc1b351d111d36f3ca7e72fbaa7fd31eb638 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 425ee3c2cc064b08f4594d5124440bf936d4a65a..6846cd693ff39109334a200e0c95e58ee20370ca 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 {