diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp
index 4f234a58e7..774c619cfc 100644
--- a/src/qe/lite/qe_lite_tactic.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -2467,6 +2467,7 @@ private:
             cur_vals[i] = var_lbs[i];
 
         var_subst vs(m, false);
+        inv_var_shifter shift(m);
         expr_ref_vector disjuncts(m);
 
         while (true) {
@@ -2479,6 +2480,7 @@ private:
             for (expr* p : payload) {
                 expr_ref inst(m);
                 inst = vs(p, subst_map.size(), subst_map.data());
+                shift(inst, num_decls, inst);
                 inst_conjs.push_back(inst);
             }
             expr_ref inst_body(m);
diff --git a/src/test/smt_context.cpp b/src/test/smt_context.cpp
index d7297c9d0a..215f3285cc 100644
--- a/src/test/smt_context.cpp
+++ b/src/test/smt_context.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "smt/smt_context.h"
 #include "ast/reg_decl_plugins.h"
+#include "ast/arith_decl_plugin.h"
 
 void tst_smt_context()
 {
@@ -34,4 +35,31 @@ void tst_smt_context()
     }
 
     ctx.check();
+
+    {
+        arith_util a(m);
+        expr_ref x(m.mk_var(2, a.mk_int()), m);
+        expr_ref x4(m.mk_var(1, a.mk_int()), m);
+        expr_ref y(m.mk_var(0, a.mk_int()), m);
+        expr_ref zero(a.mk_int(0), m);
+        expr_ref two(a.mk_int(2), m);
+        expr_ref_vector conjs(m);
+        conjs.push_back(a.mk_gt(x, y));
+        conjs.push_back(a.mk_gt(zero, x4));
+        conjs.push_back(a.mk_gt(zero, a.mk_uminus(y)));
+        conjs.push_back(a.mk_lt(zero, a.mk_uminus(a.mk_mul(two, y))));
+        expr_ref body(m.mk_and(conjs), m);
+
+        sort* y_sort = a.mk_int();
+        symbol y_name("y");
+        body = m.mk_exists(1, &y_sort, &y_name, body);
+
+        sort* sorts[2] = { a.mk_int(), a.mk_int() };
+        symbol names[2] = { symbol("x"), symbol("x4") };
+        expr_ref q(m.mk_forall(2, sorts, names, body), m);
+
+        smt::context qctx(m, params);
+        qctx.assert_expr(q);
+        VERIFY(l_false == qctx.check());
+    }
 }