From db87f2aab055ab189a6c47cd9e2c4216fc65cf3f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Jul 2019 15:28:21 +0700
Subject: [PATCH] separate rewriter used by smt context from asserted formulas
 to avoid term substitution, exposed by #2370

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/asserted_formulas.h | 2 +-
 src/smt/smt_context.cpp     | 2 ++
 src/smt/smt_context.h       | 3 ++-
 src/smt/theory_arith_core.h | 1 +
 4 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index 32e1fabc7..1d2f3f998 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -244,7 +244,7 @@ public:
     expr *  get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); }
     proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); }
     
-    th_rewriter & get_rewriter() { return m_rewriter; }
+    params_ref const& get_params() const { return m_params; }
     void get_assertions(ptr_vector<expr> & result) const;
     bool empty() const { return m_formulas.empty(); }
     void display(std::ostream & out) const;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 1c0d91534..3e1b165b4 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -47,6 +47,7 @@ namespace smt {
         m_params(_p),
         m_setup(*this, p),
         m_asserted_formulas(m, p, _p),
+        m_rewriter(m),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
         m_model_generator(alloc(model_generator, m)),
         m_relevancy_propagator(mk_relevancy_propagator(*this)),
@@ -94,6 +95,7 @@ namespace smt {
         SASSERT(m_search_lvl == 0);
 
         m_case_split_queue = mk_case_split_queue(*this, p);
+        m_rewriter.updt_params(m_asserted_formulas.get_params());
 
         init();
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 8cda47983..a1928ff15 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -85,6 +85,7 @@ namespace smt {
         setup                       m_setup;
         timer                       m_timer;
         asserted_formulas           m_asserted_formulas;
+        th_rewriter                 m_rewriter;
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
@@ -261,7 +262,7 @@ namespace smt {
         }
 
         th_rewriter & get_rewriter() {
-            return m_asserted_formulas.get_rewriter();
+            return m_rewriter;
         }
 
         smt_params & get_fparams() {
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index d148daaa1..398bc3b3d 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -426,6 +426,7 @@ namespace smt {
         bool negated;
 
         s(ante, s_ante);
+
         if (ctx.get_cancel_flag()) return;
         negated = m.is_not(s_ante, s_ante_n);
         if (negated) s_ante = s_ante_n;