diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp
index 2427c9c25..11bca0133 100644
--- a/src/ast/substitution/substitution.cpp
+++ b/src/ast/substitution/substitution.cpp
@@ -172,14 +172,14 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
             unsigned num_vars = q->get_num_decls();
             substitution subst(m_manager);
             expr_ref er(m_manager);
-            subst.reserve(m_subst.offsets_capacity(), m_subst.vars_capacity());
+            subst.reserve(m_subst.offsets_capacity(), m_subst.vars_capacity() + num_vars);
             var_shifter var_sh(m_manager);
             expr_offset r;
             for (unsigned i = 0; i < m_subst.offsets_capacity(); i++) {
                 for (unsigned j = 0; j < m_subst.vars_capacity(); j++) {
                     if (find(j, i, r)) {
                         var_sh(r.get_expr(), num_vars, er);
-                        subst.insert(j, i, expr_offset(er, r.get_offset()));
+                        subst.insert(j + num_vars, i, expr_offset(er, r.get_offset()));
                     }
                 }
             }
diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp
index 889666972..0d7fb5856 100644
--- a/src/test/substitution.cpp
+++ b/src/test/substitution.cpp
@@ -20,9 +20,11 @@ void tst_substitution()
 
     var_ref v1(m.mk_var(0, m.mk_bool_sort()), m);
     var_ref v2(m.mk_var(1, m.mk_bool_sort()), m);
+    var_ref v3(m.mk_var(2, m.mk_bool_sort()), m);
+    var_ref v4(m.mk_var(3, m.mk_bool_sort()), m);
 
     substitution subst(m);
-    subst.reserve(1,2);
+    subst.reserve(1,4);
     unifier unif(m);
 
     bool ok1 = unif(v1.get(), v2.get(), subst, false);
@@ -34,4 +36,16 @@ void tst_substitution()
     TRACE("substitution", tout << ok1 << " " << ok2 << "\n";);
     subst.display(std::cout);
     subst.apply(v1.get(), res);
+    TRACE("substitution", tout << mk_pp(res, m) << "\n";);
+
+    expr_ref q(m), body(m);
+    sort_ref_vector sorts(m);
+    svector<symbol> names;
+    sorts.push_back(m.mk_bool_sort());
+    names.push_back(symbol("dude"));
+    body = m.mk_and(m.mk_eq(v1,v2), m.mk_eq(v3,v4));
+    q = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), body);
+    subst.apply(q, res);
+    TRACE("substitution", tout << mk_pp(q, m) << "\n->\n" << mk_pp(res, m) << "\n";);
+
 }