From 352912c6b55448e348e97f9a69c27df580a65455 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Mar 2013 21:06:13 -0800
Subject: [PATCH] add default simplifications as tactic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/horn_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

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());