diff --git a/build.sbt b/build.sbt
index 43a9a691284bd1ac292c46db4cfe749d2937f4ab..8fc2342f05f6c61d275d6e09c90a22e272329ffe 100644
--- a/build.sbt
+++ b/build.sbt
@@ -142,7 +142,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
 
 lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
 
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "6b74fb332416d470e0be7bf6e94ebc18fd300c2f")
+lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "cee5129e483515d7011134df669b450b92e6f871")
 
 lazy val root = (project in file(".")).
   configs(RegressionTest).
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index df167148eebd13b05a4fd69267506a49071aa823..6f849908ec27d5c3c36e029296ab968a2ade0e3a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -9,7 +9,7 @@ import Definitions._
 import Constructors._
 import DefOps.typedTransitiveCallees
 import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import smtlib.parser.Terms.{Exists => SMTExists, ForAll => SMTForall, _ }
+import smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
 import smtlib.theories.Core.Equals
 
 // This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index dfe6df71419ff6b9fc817fe3525b72335a3cad5f..801a71662c2c6b37e519c0f4bf43b79b61a11b72 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -14,7 +14,7 @@ import Extractors._
 import Constructors._
 import Types._
 
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, ForAll => SMTForall, _}
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Forall => SMTForall, _}
 import _root_.smtlib.parser.Commands._
 import _root_.smtlib.interpreters.CVC4Interpreter
 import _root_.smtlib.theories._
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 26fb3d9a1e39204bf7a047a44983ebad8f2053ae..942faa10808624bdb9138920967f1fcfd27e0bf8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -18,7 +18,7 @@ import _root_.smtlib.common._
 import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
 import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _}
 import _root_.smtlib.parser.Terms.{
-  ForAll => SMTForall,
+  Forall => SMTForall,
   Exists => SMTExists,
   Identifier => SMTIdentifier,
   Let => SMTLet,
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 8a39d9fbb1bd33e86ab720d6b446d71942941ec7..dc91864b686ab05594051ea031b196122fe83f5a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -9,7 +9,7 @@ import Definitions._
 import Expressions._
 import Constructors._
 import smtlib.parser.Commands.{Assert => SMTAssert}
-import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
+import smtlib.parser.Terms.{Forall => SMTForall, SSymbol}
 
 /**
  * This solver models function definitions as universally quantified formulas.