diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9a06cff266e221b0459b7d23e9417b4940ec5743..d936a4e3ac73612e62fa15e4eb3ba15102d1c6fb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -309,12 +309,19 @@ trait AbstractZ3Solver extends Solver {
         newAST
       }
       case v @ Variable(id) => z3Vars.get(id) match {
-        case Some(ast) => ast
+        case Some(ast) => 
+          ast
         case None => {
-          val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
-          z3Vars = z3Vars + (id -> newAST)
-          variables += (v -> newAST)
-          newAST
+          variables.getB(v) match {
+            case Some(ast) =>
+              ast
+
+            case None =>
+              val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
+              z3Vars = z3Vars + (id -> newAST)
+              variables += (v -> newAST)
+              newAST
+          }
         }
       }