use scala-smtlib from official repo

build.sbt

@@ -42,7 +42,8 @@ libraryDependencies ++= Seq(
   "info.hupel" %% "pide-2015" % libisabelleVersion,
   "org.slf4j" % "slf4j-nop" % "1.7.13",
   "org.ow2.asm" % "asm-all" % "5.0.4",
-  "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2"
+  "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2",
+  "com.regblanc" %% "scala-smtlib" % "0.2"
 )
 
 lazy val scriptName = "leon"
@@ -169,11 +170,10 @@ parallelExecution in GenCTest := false
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "372bb14d0c84953acc17f9a7e1592087adb0a3e1")
 
 lazy val root = (project in file(".")).
   configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
-  dependsOn(bonsai, scalaSmtLib).
+  dependsOn(bonsai).
   settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -31,7 +31,7 @@ import _root_.smtlib.parser.Terms.{
   _
 }
 import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
-import _root_.smtlib.theories._
+import _root_.smtlib.theories.{Constructors => SmtLibConstructors, _}
 import _root_.smtlib.theories.experimental._
 import _root_.smtlib.interpreters.ProcessInterpreter
 
@@ -415,7 +415,7 @@ trait SMTLIBTarget extends Interruptible {
           case more =>
             val es = freshSym("e")
             SMTLet(VarBinding(es, toSMT(e)), Seq(),
-              Core.Or(oneOf.map(FunctionApplication(_, Seq(es: Term))): _*))
+              SmtLibConstructors.or(oneOf.map(FunctionApplication(_, Seq(es: Term)))))
         }
 
       case CaseClass(cct, es) =>
@@ -615,8 +615,8 @@ trait SMTLIBTarget extends Interruptible {
       case RealTimes(a, b)           => Reals.Mul(toSMT(a), toSMT(b))
       case RealDivision(a, b)        => Reals.Div(toSMT(a), toSMT(b))
 
-      case And(sub)                  => Core.And(sub.map(toSMT): _*)
-      case Or(sub)                   => Core.Or(sub.map(toSMT): _*)
+      case And(sub)                  => SmtLibConstructors.and(sub.map(toSMT))
+      case Or(sub)                   => SmtLibConstructors.or(sub.map(toSMT))
       case IfExpr(cond, thenn, elze) => Core.ITE(toSMT(cond), toSMT(thenn), toSMT(elze))
       case f @ FunctionInvocation(_, sub) =>
         if (sub.isEmpty) declareFunction(f.tfd) else {