diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 1f0b760d70c59796cd7cdb5a9272526077bda087..281310a819a206ce626496045edc58c2b09ed113 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -30,7 +30,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
 
   // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
   override def assertCnstr(e: Expr) = try {
-    sendCommand(SMTAssert(quantifiedTerm(SMTExists, e)))
+    sendCommand(SMTAssert(quantifiedTerm(SMTExists, e)(Map())))
   } catch {
     case _ : SolverUnsupportedError =>
       addError()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 232867dcc3896a935fff05127dfe944a59f43822..382122cba66859e68810bfce2f2b26aae83f40f0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -100,7 +100,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
           application(post, Seq(tfd.applied))
         )
         try {
-          sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
+          sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)(Map())))
         } catch {
           case _ : SolverUnsupportedError =>
             addError()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index aa18becd2b2416fa7a72d74573f28652217b13ee..f82df1a3bc35f44bc2088a7983e680d6d42bfa9b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -141,8 +141,10 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
     quantifier: (SortedVar, Seq[SortedVar], Term) => Term,
     vars: Seq[Identifier],
     body: Expr
-  ) : Term = {
-    if (vars.isEmpty) toSMT(body)(Map())
+  )(
+    implicit bindings: Map[Identifier, Term]
+  ): Term = {
+    if (vars.isEmpty) toSMT(body)
     else {
       val sortedVars = vars map { id =>
         SortedVar(id2sym(id), declareSort(id.getType))
@@ -150,13 +152,15 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
       quantifier(
         sortedVars.head,
         sortedVars.tail,
-        toSMT(body)(vars.map{ id => id -> (id2sym(id): Term)}.toMap)
+        toSMT(body)(bindings ++ vars.map{ id => id -> (id2sym(id): Term)})
       )
     }
   }
 
   // Returns a quantified term where all free variables in the body have been quantified
-  protected def quantifiedTerm(quantifier: (SortedVar, Seq[SortedVar], Term) => Term, body: Expr): Term =
+  protected def quantifiedTerm(quantifier: (SortedVar, Seq[SortedVar], Term) => Term, body: Expr)(
+    implicit bindings: Map[Identifier, Term]
+  ): Term =
     quantifiedTerm(quantifier, variablesOf(body).toSeq, body)
 
   protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 2ec571f1ea2b0580cbb1eef697610256a1e61dc5..9a8e60e6b7aa916703804d617ec5b3cd3bcd27ad 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -47,7 +47,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
           FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
           tfd.body.get
         )
-      )
+      )(Map())
       sendCommand(SMTAssert(term))
     }
 
@@ -62,7 +62,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
         application(post, Seq(tfd.applied))
       )
       try {
-        sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
+        sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)(Map())))
       } catch {
         case _ : SolverUnsupportedError =>
           addError()