diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index a8ace78aa..cd03e522e 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -287,6 +287,7 @@ class horn_tactic : public tactic {
             expr_substitution sub(m);
             sub.insert(q, m.mk_false());
             scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+            rep->set_substitution(&sub);
             g->inc_depth();
             g->reset();
             result.push_back(g.get());