From 5845958986611889fb64516c670571aed75eeb4e Mon Sep 17 00:00:00 2001
From: Sangwoo Joh <swjoh@ropas.snu.ac.kr>
Date: Thu, 24 Aug 2017 18:17:47 +0900
Subject: [PATCH 01/10] Bugfix: get_objectives in ML API

---
 src/api/ml/z3.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index c4a4da00c..46fe5bd6d 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1964,7 +1964,7 @@ struct
   let from_file (x:optimize) (s:string) = Z3native.optimize_from_file (gc x) x s
   let from_string (x:optimize) (s:string) = Z3native.optimize_from_string (gc x) x s
   let get_assertions (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_assertions (gc x) x)
-  let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_statistics (gc x) x)
+  let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_objectives (gc x) x)
 end
 
 

From ed4477c9e410b688bfc84bcb44e6f104f1add9fe Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 18:32:50 +0100
Subject: [PATCH 02/10] Whitespace

---
 src/ast/macros/macro_manager.h | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index a0a42b790..b72c1e6bf 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -52,12 +52,12 @@ class macro_manager {
         unsigned m_forbidden_lim;
     };
     svector<scope>                   m_scopes;
-    
+
     func_decl_dependencies           m_deps;
 
     void restore_decls(unsigned old_sz);
     void restore_forbidden(unsigned old_sz);
-    
+
     class macro_expander : public simplifier {
     protected:
         macro_manager &   m_macro_manager;
@@ -91,8 +91,8 @@ public:
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; }
     void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
     void expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr);
-    
-    
+
+
 };
 
 #endif /* MACRO_MANAGER_H_ */

From 227e6801c2276929c3b3242e97d23f55b993491f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 18:33:21 +0100
Subject: [PATCH 03/10] Whitespace

---
 src/tactic/ufbv/macro_finder_tactic.cpp | 44 ++++++++++++-------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 9b1835ff3..e1e3b669b 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -26,24 +26,24 @@ Notes:
 #include "tactic/extension_model_converter.h"
 #include "tactic/ufbv/macro_finder_tactic.h"
 
-class macro_finder_tactic : public tactic {    
+class macro_finder_tactic : public tactic {
 
     struct imp {
         ast_manager & m_manager;
         bool m_elim_and;
 
-        imp(ast_manager & m, params_ref const & p) : 
+        imp(ast_manager & m, params_ref const & p) :
             m_manager(m),
             m_elim_and(false) {
             updt_params(p);
         }
-        
+
         ast_manager & m() const { return m_manager; }
-        
-        
-        void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
+
+
+        void operator()(goal_ref const & g,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
@@ -63,20 +63,20 @@ class macro_finder_tactic : public tactic {
             bv_simplifier_params bv_params;
             bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
             simp.register_plugin(bvsimp);
-                
+
             macro_manager mm(m_manager, simp);
             macro_finder mf(m_manager, mm);
-            
+
             expr_ref_vector forms(m_manager), new_forms(m_manager);
-            proof_ref_vector proofs(m_manager), new_proofs(m_manager);            
+            proof_ref_vector proofs(m_manager), new_proofs(m_manager);
             unsigned   size = g->size();
             for (unsigned idx = 0; idx < size; idx++) {
                 forms.push_back(g->form(idx));
-                proofs.push_back(g->pr(idx));                
+                proofs.push_back(g->pr(idx));
             }
 
             mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
-        
+
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
                 g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
@@ -89,7 +89,7 @@ class macro_finder_tactic : public tactic {
                 evmc->insert(f, f_interp);
             }
             mc = evmc;
-                        
+
             g->inc_depth();
             result.push_back(g.get());
             TRACE("macro-finder", g->display(tout););
@@ -102,7 +102,7 @@ class macro_finder_tactic : public tactic {
     };
 
     imp *      m_imp;
-    params_ref m_params;    
+    params_ref m_params;
 public:
     macro_finder_tactic(ast_manager & m, params_ref const & p):
         m_params(p) {
@@ -112,7 +112,7 @@ public:
     virtual tactic * translate(ast_manager & m) {
         return alloc(macro_finder_tactic, m, m_params);
     }
-        
+
     virtual ~macro_finder_tactic() {
         dealloc(m_imp);
     }
@@ -128,19 +128,19 @@ public:
         insert_produce_proofs(r);
         r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier.");
     }
-    
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-    
+
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
         imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }
 

From ed8c11ff76229e1bcc1987a155f8765e1e763533 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 19:59:38 +0100
Subject: [PATCH 04/10] Whitespace

---
 src/smt/smt_model_finder.cpp | 400 +++++++++++++++++------------------
 1 file changed, 200 insertions(+), 200 deletions(-)

diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 73d1e9f22..94a6a7267 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -84,8 +84,8 @@ namespace smt {
             expr_mark               m_visited;
         public:
             instantiation_set(ast_manager & m):m_manager(m) {}
-            
-            ~instantiation_set() {  
+
+            ~instantiation_set() {
                 for (auto const& kv : m_elems) {
                     m_manager.dec_ref(kv.m_key);
                 }
@@ -110,7 +110,7 @@ namespace smt {
                 m_elems.erase(n);
                 m_manager.dec_ref(n);
             }
-            
+
             void display(std::ostream & out) const {
                 for (auto const& kv : m_elems) {
                     out << mk_bounded_pp(kv.m_key, m_manager) << " [" << kv.m_value << "]\n";
@@ -126,7 +126,7 @@ namespace smt {
                 m_inv.find(v, t);
                 return t;
             }
-            
+
             unsigned get_generation(expr * t) const {
                 unsigned gen = 0;
                 m_elems.find(t, gen);
@@ -187,15 +187,15 @@ namespace smt {
         };
 
         /**
-           During model construction time, 
+           During model construction time,
            we solve several constraints that impose restrictions
            on how the model for the ground formulas may be extended to
            a model to the relevant universal quantifiers.
-           
+
            The class node and its subclasses are used to solve
            these constraints.
         */
-        
+
         // -----------------------------------
         //
         // nodes
@@ -209,14 +209,14 @@ namespace smt {
             unsigned            m_id;
             node *              m_find;
             unsigned            m_eqc_size;
-            
+
             sort *              m_sort; // sort of the elements in the instantiation set.
-            
+
             bool                m_mono_proj;     // relevant for integers & reals & bit-vectors
             bool                m_signed_proj;   // relevant for bit-vectors.
             ptr_vector<node>    m_avoid_set;
             ptr_vector<expr>    m_exceptions;
-            
+
             instantiation_set * m_set;
 
             expr *              m_else;
@@ -286,7 +286,7 @@ namespace smt {
                 if (!ex.contains(n))
                     ex.push_back(n);
             }
-            
+
             void set_mono_proj() {
                 get_root()->m_mono_proj = true;
             }
@@ -348,7 +348,7 @@ namespace smt {
             instantiation_set * get_instantiation_set() { return get_root()->m_set; }
 
             ptr_vector<expr> const & get_exceptions() const { return get_root()->m_exceptions; }
-            
+
             ptr_vector<node> const & get_avoid_set() const { return get_root()->m_avoid_set; }
 
             // return true if m_avoid_set.contains(this)
@@ -366,8 +366,8 @@ namespace smt {
                 SASSERT(get_root()->m_else == 0);
                 get_root()->m_else = e;
             }
-            
-            expr * get_else() const { 
+
+            expr * get_else() const {
                 return get_root()->m_else;
             }
 
@@ -375,7 +375,7 @@ namespace smt {
                 SASSERT(get_root()->m_proj == 0);
                 get_root()->m_proj = f;
             }
-            
+
             func_decl * get_proj() const {
                 return get_root()->m_proj;
             }
@@ -384,7 +384,7 @@ namespace smt {
         typedef std::pair<ast *, unsigned> ast_idx_pair;
         typedef pair_hash<obj_ptr_hash<ast>, unsigned_hash> ast_idx_pair_hash;
         typedef map<ast_idx_pair, node *, ast_idx_pair_hash, default_eq<ast_idx_pair> > key2node;
-        
+
         /**
            \brief Auxiliary class for processing the "Almost uninterpreted fragment" described in the paper:
            Complete instantiation for quantified SMT formulas
@@ -402,16 +402,16 @@ namespace smt {
 
             context *                 m_context;
 
-            // Mapping from sort to auxiliary constant. 
-            // This auxiliary constant is used as a "witness" that is asserted as different from a 
-            // finite number of terms. 
+            // Mapping from sort to auxiliary constant.
+            // This auxiliary constant is used as a "witness" that is asserted as different from a
+            // finite number of terms.
             // It is only safe to use this constant for infinite sorts.
-            obj_map<sort, app *>      m_sort2k; 
+            obj_map<sort, app *>      m_sort2k;
             expr_ref_vector           m_ks; // range of m_sort2k
-            
+
             // Support for evaluating expressions in the current model.
             proto_model *             m_model;
-            obj_map<expr, expr *>     m_eval_cache[2];            
+            obj_map<expr, expr *>     m_eval_cache[2];
             expr_ref_vector           m_eval_cache_range;
 
             ptr_vector<node>          m_root_nodes;
@@ -428,7 +428,7 @@ namespace smt {
                 m_eval_cache[1].reset();
                 m_eval_cache_range.reset();
             }
-            
+
             node * mk_node(key2node & m, ast * n, unsigned i, sort * s) {
                 node * r = 0;
                 ast_idx_pair k(n, i);
@@ -482,18 +482,18 @@ namespace smt {
                 flush_nodes();
                 reset_eval_cache();
             }
-        
+
             void set_context(context * ctx) {
                 SASSERT(m_context==0);
                 m_context = ctx;
             }
-            
+
             ast_manager & get_manager() const { return m_manager; }
-            
+
             arith_simplifier_plugin * get_arith_simp() const { return m_asimp; }
 
             bv_simplifier_plugin * get_bv_simp() const { return m_bvsimp; }
-            
+
             void reset() {
                 flush_nodes();
                 m_nodes.reset();
@@ -509,21 +509,21 @@ namespace smt {
                 m_model = m;
             }
 
-            proto_model * get_model() const { 
+            proto_model * get_model() const {
                 SASSERT(m_model);
                 return m_model;
             }
-            
-            node * get_uvar(quantifier * q, unsigned i) { 
+
+            node * get_uvar(quantifier * q, unsigned i) {
                 SASSERT(i < q->get_num_decls());
                 sort * s = q->get_decl_sort(q->get_num_decls() - i - 1);
-                return mk_node(m_uvars, q, i, s); 
+                return mk_node(m_uvars, q, i, s);
             }
 
-            node * get_A_f_i(func_decl * f, unsigned i) { 
+            node * get_A_f_i(func_decl * f, unsigned i) {
                 SASSERT(i < f->get_arity());
                 sort * s = f->get_domain(i);
-                return mk_node(m_A_f_is, f, i, s); 
+                return mk_node(m_A_f_is, f, i, s);
             }
 
             instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const {
@@ -534,7 +534,7 @@ namespace smt {
                     return r->get_instantiation_set();
                 return 0;
             }
-            
+
             void mk_instantiation_sets() {
                 for (node* curr : m_nodes) {
                     if (curr->is_root()) {
@@ -566,7 +566,7 @@ namespace smt {
 
             void display_nodes(std::ostream & out) const {
                 display_key2node(out, m_uvars);
-                display_A_f_is(out);           
+                display_A_f_is(out);
                 for (node* n : m_nodes) {
                     n->display(out, m_manager);
                 }
@@ -599,13 +599,13 @@ namespace smt {
             void collect_exceptions_values(node * n, ptr_buffer<expr> & r) {
                 ptr_vector<expr> const & exceptions   = n->get_exceptions();
                 ptr_vector<node> const & avoid_set    = n->get_avoid_set();
-                
+
                 for (expr* e : exceptions) {
                     expr * val = eval(e, true);
                     SASSERT(val != 0);
                     r.push_back(val);
                 }
-                
+
                 for (node* a : avoid_set) {
                     node * n = a->get_root();
                     if (!n->is_mono_proj() && n->get_else() != 0) {
@@ -628,7 +628,7 @@ namespace smt {
                 obj_map<expr, unsigned> const & elems = s->get_elems();
 
                 expr *    t_result   = 0;
-                unsigned  gen_result = UINT_MAX; 
+                unsigned  gen_result = UINT_MAX;
                 for (auto const& kv : elems) {
                     expr *     t = kv.m_key;
                     unsigned gen = kv.m_value;
@@ -651,13 +651,13 @@ namespace smt {
 
             bool is_infinite(sort * s) const {
                 // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
-                return 
+                return
                     !m_manager.is_uninterp(s) &&
                     s->is_infinite();
             }
 
             /**
-               \brief Return a fresh constant k that is used as a witness for elements that must be different from 
+               \brief Return a fresh constant k that is used as a witness for elements that must be different from
                a set of values.
             */
             app * get_k_for(sort * s) {
@@ -674,7 +674,7 @@ namespace smt {
 
             /**
                \brief Get the interpretation for k in m_model.
-               If m_model does not provide an interpretation for k, then 
+               If m_model does not provide an interpretation for k, then
                create a fresh one.
 
                Remark: this method uses get_fresh_value, so it may fail.
@@ -717,7 +717,7 @@ namespace smt {
                 }
                 return true;
             }
-            
+
             void set_projection_else(node * n) {
                 SASSERT(n->is_root());
                 SASSERT(!n->is_mono_proj());
@@ -744,7 +744,7 @@ namespace smt {
                             return;
                         }
                     }
-                    // TBD: add support for the else of bitvectors. 
+                    // TBD: add support for the else of bitvectors.
                     // Idea: get the term t with the minimal interpreation and use t - 1.
                 }
                 n->set_else((*(elems.begin())).m_key);
@@ -775,7 +775,7 @@ namespace smt {
                     expr_ref e_plus_1(m_manager);
                     expr_ref e_minus_1(m_manager);
                     TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m_manager) << "\none:\n" << mk_ismt2_pp(one, m_manager) << "\n";);
-                    ps->mk_add(e, one, e_plus_1); 
+                    ps->mk_add(e, one, e_plus_1);
                     ps->mk_sub(e, one, e_minus_1);
                     // Note: exceptions come from quantifiers bodies. So, they have generation 0.
                     n->insert(e_plus_1, 0);
@@ -865,7 +865,7 @@ namespace smt {
                 var = m_manager.mk_var(0, s);
                 for (unsigned i = sz - 1; i >= 1; i--) {
                     expr_ref c(m_manager);
-                    if (is_arith) 
+                    if (is_arith)
                         as->mk_lt(var, values[i], c);
                     else if (!is_signed)
                         bs->mk_ult(var, values[i], c);
@@ -896,7 +896,7 @@ namespace smt {
                 }
                 n->set_proj(p);
             }
-            
+
             void mk_projections() {
                 for (node * n : m_root_nodes) {
                     SASSERT(n->is_root());
@@ -906,7 +906,7 @@ namespace smt {
                         mk_simple_proj(n);
                 }
             }
-            
+
             /**
                \brief Store in r the partial functions that have A_f_i nodes.
             */
@@ -926,7 +926,7 @@ namespace smt {
                     }
                 }
             }
-            
+
             /**
                \brief Make sorts associated with nodes that must avoid themselves finite.
                Only uninterpreted sorts are considered.
@@ -938,16 +938,16 @@ namespace smt {
                 for (node * n : m_root_nodes) {
                     SASSERT(n->is_root());
                     sort * s = n->get_sort();
-                    if (m_manager.is_uninterp(s) && 
+                    if (m_manager.is_uninterp(s) &&
                         // Making all uninterpreted sorts finite.
-                        // n->must_avoid_itself() && 
+                        // n->must_avoid_itself() &&
                         !m_model->is_finite(s)) {
                         m_model->freeze_universe(s);
                     }
                 }
             }
 
-            void add_elem_to_empty_inst_sets() {                
+            void add_elem_to_empty_inst_sets() {
                 obj_map<sort, expr*> sort2elems;
                 ptr_vector<node> need_fresh;
                 for (node * n : m_root_nodes) {
@@ -956,11 +956,11 @@ namespace smt {
                     TRACE("model_finder", s->display(tout););
                     obj_map<expr, unsigned> const & elems = s->get_elems();
                     if (elems.empty()) {
-                        // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts 
+                        // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts
                         // (e.g., (Array S S) where S is uninterpreted). The problem is that these sorts do not have a fixed interpretation.
                         // Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value.
                         // If these module values "leak" inside the logical context, they may affect satisfiability.
-                        // 
+                        //
                         sort * ns = n->get_sort();
                         if (m_manager.is_fully_interp(ns)) {
                             n->insert(m_model->get_some_value(ns), 0);
@@ -998,14 +998,14 @@ namespace smt {
                         m_root_nodes.push_back(n);
                 }
             }
-            
+
             /**
                \brief Return the projection function for f at argument i.
-               Return 0, if there is none. 
+               Return 0, if there is none.
 
                \remark This method assumes that mk_projections was already
                invoked.
-               
+
                \remark f may have a non partial interpretation on m_model.
                This may happen because the evaluator uses model_completion.
                In the beginning of fix_model() we collected all f with
@@ -1022,21 +1022,21 @@ namespace smt {
                     return 0;
                 return r->get_proj();
             }
-            
+
             /**
-               \brief Complete the interpretation of the functions that were 
+               \brief Complete the interpretation of the functions that were
                collected in the beginning of fix_model().
              */
             void complete_partial_funcs(func_decl_set const & partial_funcs) {
                 for (func_decl * f : partial_funcs) {
                     // Complete the current interpretation
                     m_model->complete_partial_func(f);
-                    
+
                     unsigned arity   = f->get_arity();
                     func_interp * fi = m_model->get_func_interp(f);
                     if (fi->is_constant())
                         continue; // there is no point in using the projection for fi, since fi is the constant function.
-                    
+
                     expr_ref_vector args(m_manager);
                     bool has_proj = false;
                     for (unsigned i = 0; i < arity; i++) {
@@ -1055,7 +1055,7 @@ namespace smt {
                         func_decl *   f_aux  = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range());
                         func_interp * new_fi = alloc(func_interp, m_manager, arity);
                         new_fi->set_else(m_manager.mk_app(f_aux, args.size(), args.c_ptr()));
-                        TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" << 
+                        TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" <<
                               mk_pp(new_fi->get_else(), m_manager) << "\n";);
                         m_model->reregister_decl(f, new_fi, f_aux);
                     }
@@ -1067,7 +1067,7 @@ namespace smt {
                 instantiation_set * s                 = n->get_instantiation_set();
                 s->mk_inverse(*this);
             }
-            
+
             void mk_inverses() {
                 for (node * n : m_root_nodes) {
                     SASSERT(n->is_root());
@@ -1107,7 +1107,7 @@ namespace smt {
            information about the quantifier structure. These bits are
            instances of subclasses of qinfo.
         */
-        
+
         /**
            \brief Generic bit of information collected when analyzing quantifiers.
            The subclasses are defined in the .cpp file.
@@ -1118,7 +1118,7 @@ namespace smt {
             virtual char const * get_kind() const = 0;
             virtual bool is_equal(qinfo const * qi) const = 0;
             virtual void display(std::ostream & out) const { out << "[" << get_kind() << "]"; }
-            
+
             // AUF fragment solver
             virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) = 0;
             virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) = 0;
@@ -1139,17 +1139,17 @@ namespace smt {
             f_var(func_decl * f, unsigned i, unsigned j):m_f(f), m_arg_i(i), m_var_j(j) {}
             virtual ~f_var() {}
 
-            virtual char const * get_kind() const { 
-                return "f_var"; 
+            virtual char const * get_kind() const {
+                return "f_var";
             }
-            
+
             virtual bool is_equal(qinfo const * qi) const {
                 if (qi->get_kind() != get_kind())
                     return false;
                 f_var const * other = static_cast<f_var const *>(qi);
                 return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j;
             }
-            
+
             virtual void display(std::ostream & out) const {
                 out << "(" << m_f->get_name() << ":" << m_arg_i << " -> v!" << m_var_j << ")";
             }
@@ -1169,7 +1169,7 @@ namespace smt {
                        for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " ";
                        tout << "-> " << mk_pp(m_f->get_range(), m) << "\n";
                        );
-                                               
+
                 n1->merge(n2);
             }
 
@@ -1191,7 +1191,7 @@ namespace smt {
                         // a necessary instantiation.
                         enode * e_arg = n->get_arg(m_arg_i);
                         expr * arg    = e_arg->get_owner();
-                        A_f_i->insert(arg, e_arg->get_generation());                        
+                        A_f_i->insert(arg, e_arg->get_generation());
                     }
                 }
             }
@@ -1204,7 +1204,7 @@ namespace smt {
                     uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager());
                 instantiation_set * s = uvar_inst_sets[m_var_j];
                 SASSERT(s != 0);
-                
+
                 enode_vector::const_iterator it  = ctx->begin_enodes_of(m_f);
                 enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
                 for (; it != end; it++) {
@@ -1212,7 +1212,7 @@ namespace smt {
                     if (ctx->is_relevant(n)) {
                         enode * e_arg = n->get_arg(m_arg_i);
                         expr * arg    = e_arg->get_owner();
-                        s->insert(arg, e_arg->get_generation());                        
+                        s->insert(arg, e_arg->get_generation());
                     }
                 }
             }
@@ -1227,19 +1227,19 @@ namespace smt {
             }
             virtual ~f_var_plus_offset() {}
 
-            virtual char const * get_kind() const { 
-                return "f_var_plus_offset"; 
+            virtual char const * get_kind() const {
+                return "f_var_plus_offset";
             }
-            
+
             virtual bool is_equal(qinfo const * qi) const {
                 if (qi->get_kind() != get_kind())
                     return false;
                 f_var_plus_offset const * other = static_cast<f_var_plus_offset const *>(qi);
                 return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j && m_offset.get() == other->m_offset.get();
             }
-            
+
             virtual void display(std::ostream & out) const {
-                out << "(" << m_f->get_name() << ":" << m_arg_i << " - " << 
+                out << "(" << m_f->get_name() << ":" << m_arg_i << " - " <<
                     mk_bounded_pp(m_offset.get(), m_offset.get_manager()) << " -> v!" << m_var_j << ")";
             }
 
@@ -1330,11 +1330,11 @@ namespace smt {
 
         /**
            \brief auf_arr is a term (pattern) of the form:
-           
+
            FORM :=  GROUND-TERM
                 |   (select FORM VAR)
-                
-           Store in arrays, all enodes that match the pattern     
+
+           Store in arrays, all enodes that match the pattern
         */
         void get_auf_arrays(app * auf_arr, context * ctx, ptr_buffer<enode> & arrays) {
             if (is_ground(auf_arr)) {
@@ -1361,10 +1361,10 @@ namespace smt {
                 }
             }
         }
-        
+
         class select_var : public qinfo {
         protected:
-            ast_manager & m_manager; 
+            ast_manager & m_manager;
             array_util    m_array;
             app *         m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const
             unsigned      m_arg_i;
@@ -1384,16 +1384,16 @@ namespace smt {
             virtual ~select_var() {}
 
             virtual char const * get_kind() const {
-                return "select_var"; 
+                return "select_var";
             }
-            
+
             virtual bool is_equal(qinfo const * qi) const {
                 if (qi->get_kind() != get_kind())
                     return false;
                 select_var const * other = static_cast<select_var const *>(qi);
                 return m_select == other->m_select && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j;
             }
-            
+
             virtual void display(std::ostream & out) const {
                 out << "(" << mk_bounded_pp(m_select, m_manager) << ":" << m_arg_i << " -> v!" << m_var_j << ")";
             }
@@ -1401,12 +1401,12 @@ namespace smt {
             virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) {
                 ptr_buffer<enode> arrays;
                 get_auf_arrays(get_array(), ctx, arrays);
-                TRACE("select_var", 
+                TRACE("select_var",
                       tout << "enodes matching: "; display(tout); tout << "\n";
                       for (enode* n : arrays) {
                           tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m_manager) << "\n";
                       });
-                node * n1 = s.get_uvar(q, m_var_j);                
+                node * n1 = s.get_uvar(q, m_var_j);
                 for (enode* n : arrays) {
                     app * ground_array = n->get_owner();
                     func_decl * f = get_array_func_decl(ground_array, s);
@@ -1429,7 +1429,7 @@ namespace smt {
                         enode_vector::iterator it2  = curr->begin_parents();
                         enode_vector::iterator end2 = curr->end_parents();
                         for (; it2 != end2; ++it2) {
-                            enode * p = *it2; 
+                            enode * p = *it2;
                             if (ctx->is_relevant(p) && p->get_owner()->get_decl() == m_select->get_decl()) {
                                 SASSERT(m_arg_i < p->get_owner()->get_num_args());
                                 enode * e_arg = p->get_arg(m_arg_i);
@@ -1440,7 +1440,7 @@ namespace smt {
                 }
             }
         };
-        
+
         class var_pair : public qinfo {
         protected:
             unsigned    m_var_i;
@@ -1450,16 +1450,16 @@ namespace smt {
                 if (m_var_i > m_var_j)
                     std::swap(m_var_i, m_var_j);
             }
-            
+
             virtual ~var_pair() {}
 
             virtual bool is_equal(qinfo const * qi) const {
                 if (qi->get_kind() != get_kind())
                     return false;
                 var_pair const * other = static_cast<var_pair const *>(qi);
-                return m_var_i == other->m_var_i && m_var_j == other->m_var_j; 
+                return m_var_i == other->m_var_i && m_var_j == other->m_var_j;
             }
-            
+
             virtual void display(std::ostream & out) const {
                 out << "(" << get_kind() << ":v!" << m_var_i << ":v!" << m_var_j << ")";
             }
@@ -1494,7 +1494,7 @@ namespace smt {
                 n1->merge(n2);
             }
         };
-        
+
         class x_leq_y : public var_pair {
         public:
             x_leq_y(unsigned i, unsigned j):var_pair(i, j) {}
@@ -1513,7 +1513,7 @@ namespace smt {
         public:
             x_sleq_y(unsigned i, unsigned j):x_leq_y(i, j) {}
             virtual char const * get_kind() const { return "x_sleq_y"; }
-            
+
             virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) {
                 node * n1 = s.get_uvar(q, m_var_i);
                 node * n2 = s.get_uvar(q, m_var_j);
@@ -1522,7 +1522,7 @@ namespace smt {
                 n1->set_signed_proj();
             }
         };
-        
+
         class var_expr_pair : public qinfo {
         protected:
             unsigned    m_var_i;
@@ -1531,19 +1531,19 @@ namespace smt {
             var_expr_pair(ast_manager & m, unsigned i, expr * t):
                 m_var_i(i), m_t(t, m) {}
             ~var_expr_pair() {}
-            
+
             virtual bool is_equal(qinfo const * qi) const {
                 if (qi->get_kind() != get_kind())
                     return false;
                 var_expr_pair const * other = static_cast<var_expr_pair const *>(qi);
                 return m_var_i == other->m_var_i && m_t.get() == other->m_t.get();
             }
-            
+
             virtual void display(std::ostream & out) const {
                 out << "(" << get_kind() << ":v!" << m_var_i << ":" << mk_bounded_pp(m_t.get(), m_t.get_manager()) << ")";
             }
         };
-        
+
         class x_eq_t : public var_expr_pair {
         public:
             x_eq_t(ast_manager & m, unsigned i, expr * t):
@@ -1591,7 +1591,7 @@ namespace smt {
                 S_q_i->insert(m_t, 0);
             }
         };
-        
+
         class x_gle_t : public var_expr_pair {
         public:
             x_gle_t(ast_manager & m, unsigned i, expr * t):
@@ -1634,16 +1634,16 @@ namespace smt {
                 m_manager.inc_ref(m_cond);
                 SASSERT(!m_hint || m_cond == 0);
             }
-            
+
             ~cond_macro() {
                 m_manager.dec_ref(m_def);
                 m_manager.dec_ref(m_cond);
             }
 
             func_decl * get_f() const { return m_f; }
-            
+
             expr * get_def() const { return m_def; }
-            
+
             expr * get_cond() const { return m_cond; }
 
             bool is_unconditional() const { return m_cond == 0 || m_manager.is_true(m_cond); }
@@ -1660,7 +1660,7 @@ namespace smt {
                 out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m_manager, 6);
                 if (m_hint)
                     out << " *hint*";
-                else 
+                else
                     out << " when " << mk_bounded_pp(m_cond, m_manager, 6);
                 out << "] weight: " << m_weight;
             }
@@ -1675,7 +1675,7 @@ namespace smt {
         // -----------------------------------
 
         class quantifier_analyzer;
-        
+
         /**
            \brief Store relevant information regarding a particular universal quantifier.
            This information is populated by quantifier_analyzer.
@@ -1749,7 +1749,7 @@ namespace smt {
                        tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";);
                 SASSERT(!has_quantifiers(m_flat_q->get_expr()));
             }
-            
+
             ~quantifier_info() {
                 std::for_each(m_qinfo_vect.begin(), m_qinfo_vect.end(), delete_proc<qinfo>());
                 std::for_each(m_cond_macros.begin(), m_cond_macros.end(), delete_proc<cond_macro>());
@@ -1759,7 +1759,7 @@ namespace smt {
             bool is_auf() const { return m_is_auf; }
 
             quantifier * get_flat_q() const { return m_flat_q; }
-            
+
             bool unary_function_fragment() const {
                 unsigned sz = m_ng_decls.size();
                 if (sz > 1)
@@ -1843,7 +1843,7 @@ namespace smt {
                 if (m_uvar_inst_sets != 0)
                     return;
                 m_uvar_inst_sets = alloc(ptr_vector<instantiation_set>);
-                for (qinfo* qi : m_qinfo_vect) 
+                for (qinfo* qi : m_qinfo_vect)
                     qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx);
                 for (instantiation_set * s : *m_uvar_inst_sets) {
                     if (s != 0)
@@ -1867,7 +1867,7 @@ namespace smt {
                 }
             }
         };
-        
+
         /**
            \brief Functor used to traverse/analyze a quantifier and
            fill the structure quantifier_info.
@@ -1883,9 +1883,9 @@ namespace smt {
             quantifier_info *    m_info;
 
             typedef enum { POS, NEG } polarity;
-            
+
             polarity neg(polarity p) { return p == POS ? NEG : POS; }
-            
+
             obj_hashtable<expr>  m_pos_cache;
             obj_hashtable<expr>  m_neg_cache;
             typedef std::pair<expr *, polarity> entry;
@@ -1919,7 +1919,7 @@ namespace smt {
             bool is_zero(expr * n) const {
                 if (get_bv_simp()->is_bv(n))
                     return get_bv_simp()->is_zero_safe(n);
-                else 
+                else
                     return get_arith_simp()->is_zero_safe(n);
             }
 
@@ -1927,22 +1927,22 @@ namespace smt {
                 return m_mutil.is_times_minus_one(n, arg);
             }
 
-            bool is_le(expr * n) const { 
+            bool is_le(expr * n) const {
                 return m_mutil.is_le(n);
             }
-            
+
             bool is_le_ge(expr * n) const {
                 return m_mutil.is_le_ge(n);
             }
 
-            bool is_signed_le(expr * n) const { 
-                return m_bv_util.is_bv_sle(n); 
+            bool is_signed_le(expr * n) const {
+                return m_bv_util.is_bv_sle(n);
             }
-            
-            expr * mk_one(sort * s) { 
-                return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s); 
+
+            expr * mk_one(sort * s) {
+                return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s);
             }
-            
+
             void mk_sub(expr * t1, expr * t2, expr_ref & r) const {
                 m_mutil.mk_sub(t1, t2, r);
             }
@@ -1990,7 +1990,7 @@ namespace smt {
                 bool inv;
                 return is_var_and_ground(lhs, rhs, v, t, inv);
             }
-            
+
             bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const {
                 if (!is_app(n))
                     return false;
@@ -2024,7 +2024,7 @@ namespace smt {
                     v2 = to_var(rhs);
                     return true;
                 }
-                return 
+                return
                     (is_var_minus_var(lhs, v1, v2) && is_zero(rhs)) ||
                     (is_var_minus_var(rhs, v1, v2) && is_zero(lhs));
             }
@@ -2042,7 +2042,7 @@ namespace smt {
                     return false;
                 if (sign) {
                     bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t);
-                    CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" 
+                    CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
                            << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
                            tout << "sign: " << sign << "\n";);
                     return r;
@@ -2062,7 +2062,7 @@ namespace smt {
                                 mk_add(tmp, one, t);
                             else
                                 mk_sub(tmp, one, t);
-                            TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" 
+                            TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
                                   << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
                                   tout << "sign: " << sign << "\n";);
                             return true;
@@ -2076,19 +2076,19 @@ namespace smt {
                 m_pos_cache.reset();
                 m_neg_cache.reset();
             }
-            
-            obj_hashtable<expr> & get_cache(polarity pol) { 
-                return pol == POS ? m_pos_cache : m_neg_cache; 
+
+            obj_hashtable<expr> & get_cache(polarity pol) {
+                return pol == POS ? m_pos_cache : m_neg_cache;
             }
 
             void visit_formula(expr * n, polarity pol) {
                 if (is_ground(n))
                     return; // ground terms do not need to be visited.
                 obj_hashtable<expr> & c = get_cache(pol);
-                if (!c.contains(n)) { 
-                    m_ftodo.push_back(entry(n, pol));  
+                if (!c.contains(n)) {
+                    m_ftodo.push_back(entry(n, pol));
                     c.insert(n);
-                } 
+                }
             }
 
             void visit_term(expr * n) {
@@ -2098,7 +2098,7 @@ namespace smt {
                     m_pos_cache.insert(n);
                 }
             }
-            
+
             /**
                \brief Process unintrepreted applications.
             */
@@ -2111,14 +2111,14 @@ namespace smt {
                         insert_qinfo(alloc(f_var, t->get_decl(), i, to_var(arg)->get_idx()));
                         continue;
                     }
-                    
+
                     var * v;
                     expr_ref k(m_manager);
                     if (is_var_plus_ground(arg, v, k)) {
                         insert_qinfo(alloc(f_var_plus_offset, m_manager, t->get_decl(), i, v->get_idx(), k.get()));
                         continue;
                     }
-                    
+
                     visit_term(arg);
                 }
             }
@@ -2127,9 +2127,9 @@ namespace smt {
             /**
                \brief A term \c t is said to be a auf_select if
                it is of ther form
-               
+
                (select a i) Where:
-               
+
                where a is ground or is_auf_select(a) == true
                and the indices are ground terms or variables.
             */
@@ -2173,11 +2173,11 @@ namespace smt {
 
             void process_app(app * t) {
                 SASSERT(!is_ground(t));
-                
+
                 if (t->get_family_id() != m_manager.get_basic_family_id()) {
                     m_info->m_ng_decls.insert(t->get_decl());
                 }
-                
+
                 if (is_uninterp(t)) {
                     process_u_app(t);
                 }
@@ -2185,19 +2185,19 @@ namespace smt {
                     process_i_app(t);
                 }
             }
-            
+
             void process_terms_on_stack() {
                 while (!m_ttodo.empty()) {
                     expr * curr = m_ttodo.back();
                     m_ttodo.pop_back();
-                    
+
                     if (m_manager.is_bool(curr)) {
                         // formula nested in a term.
                         visit_formula(curr, POS);
                         visit_formula(curr, NEG);
                         continue;
                     }
-                    
+
                     if (is_app(curr)) {
                         process_app(to_app(curr));
                     }
@@ -2215,7 +2215,7 @@ namespace smt {
                 CTRACE("model_finder_bug", is_ground(atom), tout << mk_pp(atom, m_manager) << "\n";);
                 SASSERT(!is_ground(atom));
                 SASSERT(m_manager.is_bool(atom));
-                
+
                 if (is_var(atom)) {
                     if (sign) {
                         // atom (not X) can be viewed as X != true
@@ -2227,7 +2227,7 @@ namespace smt {
                     }
                     return;
                 }
-                
+
                 if (is_app(atom)) {
                     var * v, * v1, * v2;
                     expr_ref t(m_manager);
@@ -2259,18 +2259,18 @@ namespace smt {
                     }
                     return;
                 }
-                
+
                 SASSERT(is_quantifier(atom));
                 UNREACHABLE();
             }
 
-            void process_literal(expr * atom, polarity pol) { 
-                process_literal(atom, pol == NEG); 
+            void process_literal(expr * atom, polarity pol) {
+                process_literal(atom, pol == NEG);
             }
-            
+
             void process_or(app * n, polarity p) {
                 unsigned num_args = n->get_num_args();
-                for (unsigned i = 0; i < num_args; i++) 
+                for (unsigned i = 0; i < num_args; i++)
                     visit_formula(n->get_arg(i), p);
             }
 
@@ -2291,7 +2291,7 @@ namespace smt {
             void checkpoint() {
                 m_mf.checkpoint("quantifier_analyzer");
             }
-            
+
             void process_formulas_on_stack() {
                 while (!m_ftodo.empty()) {
                     checkpoint();
@@ -2351,7 +2351,7 @@ namespace smt {
                 SASSERT(m_manager.is_bool(n));
                 visit_formula(n, POS);
             }
-            
+
             void process_clause(expr * cls) {
                 SASSERT(is_clause(m_manager, cls));
                 unsigned num_lits = get_clause_num_literals(m_manager, cls);
@@ -2371,25 +2371,25 @@ namespace smt {
                 m_mutil.collect_macro_candidates(q, candidates);
                 unsigned num_candidates = candidates.size();
                 for (unsigned i = 0; i < num_candidates; i++) {
-                    cond_macro * m = alloc(cond_macro, m_manager, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), 
+                    cond_macro * m = alloc(cond_macro, m_manager, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),
                                            candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight());
                     m_info->insert_macro(m);
                 }
             }
-            
- 
+
+
         public:
             quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s):
                 m_mf(mf),
                 m_manager(m),
                 m_mutil(m, s),
-                m_array_util(m), 
+                m_array_util(m),
                 m_arith_util(m),
                 m_bv_util(m),
                 m_info(0) {
             }
-            
-                
+
+
             void operator()(quantifier_info * d) {
                 m_info = d;
                 quantifier * q = d->get_flat_q();
@@ -2398,7 +2398,7 @@ namespace smt {
                 reset_cache();
                 SASSERT(m_ttodo.empty());
                 SASSERT(m_ftodo.empty());
-                
+
                 if (is_clause(m_manager, e)) {
                     process_clause(e);
                 }
@@ -2412,7 +2412,7 @@ namespace smt {
                 }
 
                 collect_macro_candidates(q);
-                
+
                 m_info = 0;
             }
 
@@ -2452,7 +2452,7 @@ namespace smt {
                 m_q2info(q2i),
                 m_model(0) {
             }
-            
+
             virtual ~base_macro_solver() {}
 
             /**
@@ -2470,13 +2470,13 @@ namespace smt {
             }
         };
 
-        
+
         /**
            \brief The simple macro solver satisfies quantifiers that contain
            (conditional) macros for a function f that does not occur in any other quantifier.
-           
+
            Since f does not occur in any other quantifier, I don't need to track the dependencies
-           of f. That is, recursive definition cannot be created. 
+           of f. That is, recursive definition cannot be created.
         */
         class simple_macro_solver : public base_macro_solver {
         protected:
@@ -2511,7 +2511,7 @@ namespace smt {
                         // I know the (partial) interpretation of f satisfied the ground part.
                         // MBQI will force extra instantiations if the the (partial) interpretation of f
                         // does not satisfy the quantifier.
-                        // In all other cases the "else" of f will satisfy the quantifier. 
+                        // In all other cases the "else" of f will satisfy the quantifier.
                         set_else_interp(f, f_else);
                         TRACE("model_finder", tout << "satisfying the quantifier using simple macro:\n";
                               m->display(tout); tout << "\n";);
@@ -2547,7 +2547,7 @@ namespace smt {
               Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro.
               Then, the set Q can be satisfied using f_1 = def_1 ... f_n = d_n
               when
-              
+
               Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = d_n} (*)
 
               So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check
@@ -2583,8 +2583,8 @@ namespace smt {
             typedef obj_pair_map<func_decl, expr, quantifier_set *> q_f_def;
             typedef obj_pair_hashtable<func_decl, expr> f_def_set;
             typedef obj_hashtable<expr> expr_set;
-            typedef obj_map<func_decl, expr_set *> f2defs; 
-            
+            typedef obj_map<func_decl, expr_set *> f2defs;
+
             q_f                        m_q_f;
             q_f_def                    m_q_f_def;
             ptr_vector<quantifier_set> m_qsets;
@@ -2720,14 +2720,14 @@ namespace smt {
                     }
                 }
             }
-            
+
             static void display_quantifier_set(std::ostream & out, quantifier_set const * s) {
                 for (quantifier* q : *s) {
                     out << q->get_qid() << " ";
                 }
                 out << "\n";
             }
-            
+
             void display_qcandidates(std::ostream & out, ptr_vector<quantifier> const & qcandidates) const {
                 for (quantifier * q : qcandidates) {
                     out << q->get_qid() << " ->\n" << mk_pp(q, m_manager) << "\n";
@@ -2749,14 +2749,14 @@ namespace smt {
                     out << f->get_name() << " " << mk_pp(def, m_manager) << " ->\n"; display_quantifier_set(out, s);
                 }
             }
-            
+
             //
             // Search: main procedures
             //
 
             struct ev_handler {
                 hint_solver * m_owner;
-                
+
                 void operator()(quantifier * q, bool ins) {
                     quantifier_info * qi = m_owner->get_qinfo(q);
                     qi->set_the_one(0);
@@ -2769,7 +2769,7 @@ namespace smt {
 
 
             typedef backtrackable_set<quantifier_set, quantifier *> qset;
-            typedef backtrackable_set<quantifier_set, quantifier *, ev_handler> qsset;            
+            typedef backtrackable_set<quantifier_set, quantifier *, ev_handler> qsset;
             typedef obj_map<func_decl, expr *> f2def;
 
             qset         m_residue;
@@ -2793,7 +2793,7 @@ namespace smt {
                 }
                 out << "\n";
             }
-            
+
             bool check_satisfied_residue_invariant() {
                 DEBUG_CODE(
                     for (quantifier * q : m_satisfied) {
@@ -2805,7 +2805,7 @@ namespace smt {
                 return true;
             }
 
-            
+
             bool update_satisfied_residue(func_decl * f, expr * def) {
                 bool useful = false;
                 SASSERT(check_satisfied_residue_invariant());
@@ -2831,7 +2831,7 @@ namespace smt {
                 SASSERT(check_satisfied_residue_invariant());
                 return true;
             }
-            
+
             /**
                \brief Extract from m_residue, func_decls that can be used as macros to satisfy it.
                The candidates must not be elements of m_fs.
@@ -2861,13 +2861,13 @@ namespace smt {
                 if (depth >= GREEDY_MAX_DEPTH)
                     return; // failed
 
-                TRACE("model_finder_hint", 
+                TRACE("model_finder_hint",
                       tout << "greedy depth: " << depth << ", f: " << f->get_name() << "\n";
                       display_search_state(tout););
 
                 expr_set * s = get_f_defs(f);
                 for (expr * def : *s) {
-                    
+
                     SASSERT(!m_fs.contains(f));
 
                     m_satisfied.push_scope();
@@ -2879,7 +2879,7 @@ namespace smt {
                         greedy(depth + 1); // greedy throws exception in case of success
                         // reachable iff greedy failed.
                     }
-                    
+
                     m_satisfied.pop_scope();
                     m_residue.pop_scope();
                     m_fs.erase(f);
@@ -2892,7 +2892,7 @@ namespace smt {
             */
             void greedy(unsigned depth) {
                 if (m_residue.empty()) {
-                    TRACE("model_finder_hint", 
+                    TRACE("model_finder_hint",
                           tout << "found subset that is satisfied by macros\n";
                           display_search_state(tout););
                     throw found_satisfied_subset();
@@ -2938,7 +2938,7 @@ namespace smt {
                quantifiers in m_satisfied.
             */
             void set_interp() {
-                for (auto const& kv : m_fs) {                    
+                for (auto const& kv : m_fs) {
                     func_decl * f = kv.m_key;
                     expr * def    = kv.m_value;
                     set_else_interp(f, def);
@@ -3026,7 +3026,7 @@ namespace smt {
                     return true;
                 return false;
             }
-            
+
             cond_macro * get_macro_for(func_decl * f, quantifier * q) {
                 cond_macro * r = 0;
                 quantifier_info * qi = get_qinfo(q);
@@ -3145,13 +3145,13 @@ namespace smt {
             }
         };
     };
-    
+
     // -----------------------------------
     //
-    // model finder 
+    // model finder
     //
     // -----------------------------------
-    
+
     model_finder::model_finder(ast_manager & m, simplifier & s):
         m_manager(m),
         m_context(0),
@@ -3163,11 +3163,11 @@ namespace smt {
         m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)),
         m_new_constraints(m) {
     }
-    
+
     model_finder::~model_finder() {
         reset();
     }
-        
+
     void model_finder::checkpoint() {
         checkpoint("model_finder");
     }
@@ -3184,14 +3184,14 @@ namespace smt {
         SASSERT(info != 0);
         return info;
     }
-        
+
     void model_finder::set_context(context * ctx) {
-        SASSERT(m_context == 0); 
+        SASSERT(m_context == 0);
         m_context = ctx;
         m_auf_solver->set_context(ctx);
         m_nm_solver->set_params(ctx->get_fparams());
     }
-            
+
     void model_finder::register_quantifier(quantifier * q) {
         TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m_manager) << "\n";);
         quantifier_info * new_info = alloc(quantifier_info, *this, m_manager, q);
@@ -3200,15 +3200,15 @@ namespace smt {
         m_analyzer->operator()(new_info);
         TRACE("model_finder", tout << "after analyzer:\n"; new_info->display(tout););
     }
-    
+
     void model_finder::push_scope() {
         m_scopes.push_back(scope());
         scope & s = m_scopes.back();
         s.m_quantifiers_lim = m_quantifiers.size();
     }
-    
+
     void model_finder::restore_quantifiers(unsigned old_size) {
-        unsigned curr_size = m_quantifiers.size(); 
+        unsigned curr_size = m_quantifiers.size();
         SASSERT(old_size <= curr_size);
         for (unsigned i = old_size; i < curr_size; i++) {
             quantifier * q = m_quantifiers[i];
@@ -3219,7 +3219,7 @@ namespace smt {
         }
         m_quantifiers.shrink(old_size);
     }
-    
+
     void model_finder::pop_scope(unsigned num_scopes) {
         unsigned lvl      = m_scopes.size();
         SASSERT(num_scopes <= lvl);
@@ -3228,7 +3228,7 @@ namespace smt {
         restore_quantifiers(s.m_quantifiers_lim);
         m_scopes.shrink(new_lvl);
     }
-    
+
     void model_finder::reset() {
         m_scopes.reset();
         m_dependencies.reset();
@@ -3236,7 +3236,7 @@ namespace smt {
         SASSERT(m_q2info.empty());
         SASSERT(m_quantifiers.empty());
     }
-    
+
     void model_finder::init_search_eh() {
         // do nothing in the current version
     }
@@ -3258,12 +3258,12 @@ namespace smt {
         }
         m_auf_solver->mk_instantiation_sets();
 
-        for (quantifier * q : qs) {        
+        for (quantifier * q : qs) {
             quantifier_info * qi = get_quantifier_info(q);
             qi->populate_inst_sets(*(m_auf_solver.get()), m_context);
         }
         m_auf_solver->fix_model(m_new_constraints);
-        TRACE("model_finder", 
+        TRACE("model_finder",
               for (quantifier * q : qs) {
                   quantifier_info * qi = get_quantifier_info(q);
                   quantifier * fq = qi->get_flat_q();
@@ -3285,7 +3285,7 @@ namespace smt {
         qs.swap(new_qs);
         TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *m););
     }
-    
+
     void model_finder::process_non_auf_macros(ptr_vector<quantifier> & qs, ptr_vector<quantifier> & residue, proto_model * m) {
         ptr_vector<quantifier> new_qs;
         m_nm_solver->operator()(m, qs, new_qs, residue);
@@ -3347,12 +3347,12 @@ namespace smt {
               << "\ni: " << i << " " << flat_q->get_num_decls() - q->get_num_decls() + i << "\n";);
         if (r != 0)
             return r;
-        // quantifier was not processed by AUF solver... 
+        // quantifier was not processed by AUF solver...
         // it must have been satisfied by "macro"/"hint".
         quantifier_info * qinfo = get_quantifier_info(q);
         SASSERT(qinfo);
         SASSERT(qinfo->get_the_one() != 0);
-        
+
         return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get()));
     }
 
@@ -3373,11 +3373,11 @@ namespace smt {
         }
         return t;
     }
-    
+
     /**
        \brief Assert constraints restricting the possible values of the skolem constants can be assigned to.
        The idea is to restrict them to the values in the instantiation sets.
-    
+
        \remark q is the quantifier before flattening.
 
        Return true if something was asserted.
@@ -3425,7 +3425,7 @@ namespace smt {
                 TRACE("model_finder_bug_detail", tout << "asserting new constraint: " << mk_pp(c, m_manager) << "\n";);
                 m_context->internalize(c, true);
                 literal l(m_context->get_literal(c));
-                m_context->mark_as_relevant(l);         
+                m_context->mark_as_relevant(l);
                 // asserting it as an AXIOM
                 m_context->assign(l, b_justification());
             }

From 8310b24c521b6dac99a97a61ab74115c377db1b2 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 20:34:11 +0100
Subject: [PATCH 05/10] Eliminated the dependency of the macro-finder on the
 simplifier.

---
 src/ast/macros/macro_finder.cpp   |  43 ++++++------
 src/ast/macros/macro_finder.h     |  17 ++---
 src/ast/macros/macro_manager.cpp  |   2 +-
 src/ast/macros/macro_util.cpp     | 106 ++++++++++++------------------
 src/ast/macros/macro_util.h       |  25 ++++---
 src/ast/rewriter/arith_rewriter.h |  20 +++---
 src/ast/rewriter/poly_rewriter.h  |  57 ++++++++++++++++
 src/smt/smt_model_finder.cpp      |  37 +++++------
 8 files changed, 168 insertions(+), 139 deletions(-)

diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index 285c0e5fb..604d10b04 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -21,8 +21,9 @@ Revision History:
 #include "ast/occurs.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/rewriter/arith_rewriter.h"
 
-bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
+bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@@ -32,30 +33,30 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
 }
 
 /**
-   \brief Detect macros of the form 
+   \brief Detect macros of the form
    1- (forall (X) (= (+ (f X) (R X)) c))
    2- (forall (X) (<= (+ (f X) (R X)) c))
    3- (forall (X) (>= (+ (f X) (R X)) c))
 
    The second and third cases are first converted into
    (forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
-   and 
+   and
    (forall (X) (<= (k X) 0)) when case 2
    (forall (X) (>= (k X) 0)) when case 3
 
    For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
 */
-bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
-    arith_simplifier_plugin * as = get_arith_simp();
-    arith_util & autil = as->get_arith_util();
+    arith_rewriter & arw = m_util.get_arith_rw();
+    arith_util & au = m_util.get_arith_util();
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-    
-    if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
+
+    if (!au.is_le(body) && !au.is_ge(body) && !m_manager.is_eq(body))
         return false;
-    if (!as->is_add(to_app(body)->get_arg(0)))
+    if (!au.is_add(to_app(body)->get_arg(0)))
         return false;
     app_ref head(m_manager);
     expr_ref def(m_manager);
@@ -63,15 +64,15 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
         return false;
     app_ref new_body(m_manager);
-    
+
     if (!inv || m_manager.is_eq(body))
         new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
-    else if (as->is_le(body))
-        new_body = autil.mk_ge(head, def);
+    else if (au.is_le(body))
+        new_body = au.mk_ge(head, def);
     else
-        new_body = autil.mk_le(head, def);
+        new_body = au.mk_le(head, def);
 
-    quantifier_ref new_q(m_manager); 
+    quantifier_ref new_q(m_manager);
     new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
     proof * new_pr      = 0;
     if (m_manager.proofs_enabled()) {
@@ -82,16 +83,16 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
         return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
     }
     // is ge or le
-    // 
+    //
     TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
     func_decl * f   = head->get_decl();
     func_decl * k   = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app     = m_manager.mk_app(k, head->get_num_args(), head->get_args());
     expr_ref_buffer new_rhs_args(m_manager);
     expr_ref new_rhs2(m_manager);
-    as->mk_add(def, k_app, new_rhs2);
+    arw.mk_add(def, k_app, new_rhs2);
     expr * body1    = m_manager.mk_eq(head, new_rhs2);
-    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(0)));
+    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, au.mk_numeral(0, m_manager.get_sort(def)));
     quantifier * q1 = m_manager.update_quantifier(new_q, body1);
     expr * patterns[1] = { m_manager.mk_pattern(k_app) };
     quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2);
@@ -118,7 +119,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
    n is of the form: (forall (X) (iff (= (f X) t) def[X]))
 
    Convert it into:
-   
+
    (forall (X) (= (f X) (ite def[X] t (k X))))
    (forall (X) (not (= (k X) t)))
 
@@ -126,13 +127,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
 
    The new quantifiers and proofs are stored in new_exprs and new_prs
 */
-static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, 
+static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
                                          expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     func_decl * f = head->get_decl();
     func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app   = m.mk_app(k, head->get_num_args(), head->get_args());
     app * ite     = m.mk_ite(def, t, k_app);
-    app * body_1  = m.mk_eq(head, ite); 
+    app * body_1  = m.mk_eq(head, ite);
     app * body_2  = m.mk_not(m.mk_eq(k_app, t));
     quantifier * q1 = m.update_quantifier(q, body_1);
     expr * pats[1] = { m.mk_pattern(k_app) };
@@ -183,7 +184,7 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
             TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
             found_new_macro = true;
         }
-        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { 
+        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
             TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
             pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
             found_new_macro = true;
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 7f1b27f0e..0c292eab8 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -20,8 +20,7 @@ Revision History:
 #define MACRO_FINDER_H_
 
 #include "ast/macros/macro_manager.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
-
+#include "ast/macros/macro_util.h"
 
 bool is_macro_head(expr * n, unsigned num_decls);
 bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
@@ -34,16 +33,15 @@ inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app *
    as macros.
 */
 class macro_finder {
-    ast_manager &               m_manager; 
+    ast_manager &               m_manager;
     macro_manager &             m_macro_manager;
     macro_util &                m_util;
-    arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
-    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
-    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 
-    bool is_macro(expr * n, app_ref & head, expr_ref & def);
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
+    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const;
+    bool is_macro(expr * n, app_ref & head, expr_ref & def) const;
+    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t) const;
+    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def) const;
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
@@ -52,4 +50,3 @@ public:
 };
 
 #endif /* MACRO_FINDER_H_ */
-
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index bd330a2de..f26a87445 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -28,7 +28,7 @@ Revision History:
 macro_manager::macro_manager(ast_manager & m, simplifier & s):
     m_manager(m),
     m_simplifier(s),
-    m_util(m, s),
+    m_util(m),
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 35f2fbcfb..415e77d03 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -20,8 +20,8 @@ Revision History:
 #include "ast/macros/macro_util.h"
 #include "ast/occurs.h"
 #include "ast/ast_util.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -29,96 +29,73 @@ Revision History:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/bool_rewriter.h"
 
-macro_util::macro_util(ast_manager & m, simplifier & s):
+macro_util::macro_util(ast_manager & m):
     m_manager(m),
-    m_bv(m),
-    m_simplifier(s),
-    m_arith_simp(0),
-    m_bv_simp(0),
+    m_arith_rw(m),
+    m_arith_util(m_arith_rw.get_util()),
+    m_bv_rw(m),
+    m_bv_util(m_bv_rw.get_util()),
     m_forbidden_set(0),
     m_curr_clause(0) {
 }
 
-arith_simplifier_plugin * macro_util::get_arith_simp() const {
-    if (m_arith_simp == 0) {
-        const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
-    }
-    SASSERT(m_arith_simp != 0);
-    return m_arith_simp;
-}
-
-bv_simplifier_plugin * macro_util::get_bv_simp() const {
-    if (m_bv_simp == 0) {
-        const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("bv")));
-    }
-    SASSERT(m_bv_simp != 0);
-    return m_bv_simp;
-}
-
-
 bool macro_util::is_bv(expr * n) const {
-    return m_bv.is_bv(n);
+    return m_bv_util.is_bv(n);
 }
 
 bool macro_util::is_bv_sort(sort * s) const {
-    return m_bv.is_bv_sort(s);
+    return m_bv_util.is_bv_sort(s);
 }
 
 bool macro_util::is_add(expr * n) const {
-    return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n);
+    return m_arith_util.is_add(n) || m_bv_util.is_bv_add(n);
 }
 
 bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
-    return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg);
+    return is_app(n) && to_app(n)->get_num_args() == 2 &&
+                ((m_arith_rw.is_mul(n) && m_arith_rw.is_times_minus_one(to_app(n)->get_arg(0), arg)) ||
+                 (m_bv_rw.is_mul(n) && m_bv_rw.is_times_minus_one(to_app(n)->get_arg(0), arg)));
 }
 
 bool macro_util::is_le(expr * n) const {
-    return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+    return m_arith_util.is_le(n) || m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n);
 }
 
 bool macro_util::is_le_ge(expr * n) const {
-    return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
-}
-
-poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const {
-    if (is_bv_sort(s))
-        return get_bv_simp();
-    else
-        return get_arith_simp();
+    return m_arith_util.is_le(n) || m_arith_util.is_ge(n) ||
+           m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n);
 }
 
 app * macro_util::mk_zero(sort * s) const {
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
-    ps->set_curr_sort(s);
-    return ps->mk_zero();
+    if (is_bv_sort(s))
+        return m_bv_util.mk_numeral(rational(0), s);
+    else
+        return m_arith_util.mk_numeral(0, s);
 }
 
 void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
-    if (is_bv(t1)) {
-        r = m_bv.mk_bv_sub(t1, t2);
-    }
-    else {
-        get_arith_simp()->mk_sub(t1, t2, r);
-    }
+    if (is_bv(t1))
+        r = m_bv_util.mk_bv_sub(t1, t2);
+    else
+        r = m_arith_util.mk_sub(t1, t2);
 }
 
 void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
-    if (is_bv(t1)) {
-        r = m_bv.mk_bv_add(t1, t2);
-    }
-    else {
-        get_arith_simp()->mk_add(t1, t2, r);
-    }
+    if (is_bv(t1))
+        r = m_bv_util.mk_bv_add(t1, t2);
+    else
+        m_arith_util.mk_add(t1, t2, r);
 }
 
 void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const {
-    if (num_args == 0) {
+    if (num_args == 0)
         r = mk_zero(s);
-        return;
-    }
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
-    ps->set_curr_sort(s);
-    ps->mk_add(num_args, args, r);
+    else if (num_args == 1)
+        r = args[0];
+    else if (is_bv_sort(s))
+        m_bv_rw.mk_add(num_args, args, r);
+    else
+        m_arith_rw.mk_add(num_args, args, r);
 }
 
 /**
@@ -241,13 +218,12 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c
 
 bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const {
     // TODO: obsolete... we should move to collect_arith_macro_candidates
-    arith_simplifier_plugin * as = get_arith_simp();
-    if (!m_manager.is_eq(n) && !as->is_le(n) && !as->is_ge(n))
+    if (!m_manager.is_eq(n) && !m_arith_util.is_le(n) && !m_arith_util.is_ge(n))
         return false;
     expr * lhs = to_app(n)->get_arg(0);
     expr * rhs = to_app(n)->get_arg(1);
 
-    if (!as->is_numeral(rhs))
+    if (!m_arith_util.is_numeral(rhs))
         return false;
 
     inv = false;
@@ -272,7 +248,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
             !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
             h = arg;
         }
-        else if (h == 0 && as->is_times_minus_one(arg, neg_arg) &&
+        else if (h == 0 && m_arith_util.is_times_minus_one(arg, neg_arg) &&
                  is_macro_head(neg_arg, num_decls) &&
                  !is_forbidden(to_app(neg_arg)->get_decl()) &&
                  !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
@@ -287,11 +263,11 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
         return false;
     head = to_app(h);
     expr_ref tmp(m_manager);
-    as->mk_add(args.size(), args.c_ptr(), tmp);
+    m_arith_rw.mk_add(args.size(), args.c_ptr(), tmp);
     if (inv)
-        as->mk_sub(tmp, rhs, def);
+        m_arith_rw.mk_sub(tmp, rhs, def);
     else
-        as->mk_sub(rhs, tmp, def);
+        m_arith_rw.mk_sub(rhs, tmp, def);
     return true;
 }
 
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index d76f2f0d3..3da8accc9 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -22,12 +22,8 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/obj_hashtable.h"
-#include "ast/simplifier/simplifier.h"
-
-class poly_simplifier_plugin;
-class arith_simplifier_plugin;
-class bv_simplifier_plugin;
-class basic_simplifier_plugin;
+#include "ast/rewriter/arith_rewriter.h"
+#include "ast/rewriter/bv_rewriter.h"
 
 class macro_util {
 public:
@@ -62,10 +58,10 @@ public:
 
 private:
     ast_manager &               m_manager;
-    bv_util                     m_bv;
-    simplifier &                m_simplifier;
-    arith_simplifier_plugin *   m_arith_simp;
-    bv_simplifier_plugin    *   m_bv_simp;
+    mutable arith_rewriter      m_arith_rw;
+    arith_util &                m_arith_util;
+    mutable bv_rewriter         m_bv_rw;
+    bv_util &                   m_bv_util;
     obj_hashtable<func_decl> *  m_forbidden_set;
 
     bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@@ -94,11 +90,13 @@ private:
 
 
 public:
-    macro_util(ast_manager & m, simplifier & s);
+    macro_util(ast_manager & m);
     void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; }
 
-    arith_simplifier_plugin * get_arith_simp() const;
-    bv_simplifier_plugin * get_bv_simp() const;
+    arith_util & get_arith_util() const { return m_arith_util; }
+    bv_util & get_bv_util() const { return m_bv_util; }
+    arith_rewriter & get_arith_rw() const { return m_arith_rw; }
+    bv_rewriter & get_bv_rw() const { return m_bv_rw; }
 
     bool is_macro_head(expr * n, unsigned num_decls) const;
     bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
@@ -137,7 +135,6 @@ public:
     void mk_sub(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const;
-    poly_simplifier_plugin * get_poly_simp_for(sort * s) const;
 };
 
 #endif
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index de849dbd7..2342782c1 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -29,10 +29,10 @@ protected:
     bool        m_expand_power;
     bool        m_mul2power;
     bool        m_expand_tan;
-    
+
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
-    
+
     bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
     bool is_zero(expr * n) const { return m_util.is_zero(n); }
@@ -77,7 +77,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result);
-    
+
     bool is_reduce_power_target(expr * arg, bool is_eq);
     expr * reduce_power(expr * arg, bool is_eq);
     br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
@@ -154,16 +154,16 @@ public:
         if (mk_rem_core(arg1, arg2, result) == BR_FAILED)
             result = m().mk_app(get_fid(), OP_REM, arg1, arg2);
     }
-    
+
     br_status mk_to_int_core(expr * arg, expr_ref & result);
     br_status mk_to_real_core(expr * arg, expr_ref & result);
-    void mk_to_int(expr * arg, expr_ref & result) { 
+    void mk_to_int(expr * arg, expr_ref & result) {
         if (mk_to_int_core(arg, result) == BR_FAILED)
-            result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); 
+            result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg);
     }
-    void mk_to_real(expr * arg, expr_ref & result) { 
-        if (mk_to_real_core(arg, result) == BR_FAILED)  
-            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); 
+    void mk_to_real(expr * arg, expr_ref & result) {
+        if (mk_to_real_core(arg, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg);
     }
     br_status mk_is_int(expr * arg, expr_ref & result);
 
@@ -178,6 +178,8 @@ public:
     br_status mk_sinh_core(expr * arg, expr_ref & result);
     br_status mk_cosh_core(expr * arg, expr_ref & result);
     br_status mk_tanh_core(expr * arg, expr_ref & result);
+
+    arith_util & get_util() { return m_util; }
 };
 
 #endif
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 5d38e4b10..81c5ea132 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -159,6 +159,63 @@ public:
         expr* args[2] = { a1, a2 };
         mk_sub(2, args, result);
     }
+
+    bool is_times_minus_one(expr * n, expr * & r) const {
+        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
+            r = to_app(n)->get_arg(1);
+            return true;
+        }
+        return false;
+    }
+
+    /**
+    \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
+    \c inv = true will contain true if (- v) is found, and false otherwise.
+    */
+    bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
+        if (!is_add(n) || is_ground(n))
+            return false;
+
+        ptr_buffer<expr> args;
+        v = 0;
+        expr * curr = to_app(n);
+        bool stop = false;
+        inv = false;
+        while (!stop) {
+            expr * arg;
+            expr * neg_arg;
+            if (is_add(curr)) {
+                arg = to_app(curr)->get_arg(0);
+                curr = to_app(curr)->get_arg(1);
+            }
+            else {
+                arg = curr;
+                stop = true;
+            }
+            if (is_ground(arg)) {
+                args.push_back(arg);
+            }
+            else if (is_var(arg)) {
+                if (v != 0)
+                    return false; // already found variable
+                v = to_var(arg);
+            }
+            else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
+                if (v != 0)
+                    return false; // already found variable
+                v = to_var(neg_arg);
+                inv = true;
+            }
+            else {
+                return false; // non ground term.
+            }
+        }
+        if (v == 0)
+            return false; // did not find variable
+        SASSERT(!args.empty());
+        mk_add(args.size(), args.c_ptr(), t);
+        return true;
+    }
 };
 
 
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 94a6a7267..0a80460f5 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1873,12 +1873,12 @@ namespace smt {
            fill the structure quantifier_info.
         */
         class quantifier_analyzer {
-            model_finder&        m_mf;
+            model_finder &       m_mf;
             ast_manager &        m_manager;
             macro_util           m_mutil;
             array_util           m_array_util;
-            arith_util           m_arith_util;
-            bv_util              m_bv_util;
+            arith_util &         m_arith_util;
+            bv_util &            m_bv_util;
 
             quantifier_info *    m_info;
 
@@ -1897,14 +1897,12 @@ namespace smt {
                 m_info->insert_qinfo(qi);
             }
 
-            arith_simplifier_plugin * get_arith_simp() const { return m_mutil.get_arith_simp(); }
-            bv_simplifier_plugin * get_bv_simp() const { return m_mutil.get_bv_simp(); }
-
             bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) const {
-                return get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t);
+                return m_mutil.get_arith_rw().is_var_plus_ground(n, inv, v, t) ||
+                       m_mutil.get_bv_rw().is_var_plus_ground(n, inv, v, t);
             }
 
-            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
+            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) const {
                 bool inv;
                 TRACE("is_var_plus_ground", tout << mk_pp(n, m_manager) << "\n";
                       tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n";
@@ -1917,10 +1915,11 @@ namespace smt {
             }
 
             bool is_zero(expr * n) const {
-                if (get_bv_simp()->is_bv(n))
-                    return get_bv_simp()->is_zero_safe(n);
-                else
-                    return get_arith_simp()->is_zero_safe(n);
+                if (m_bv_util.is_bv(n))
+                    return m_bv_util.is_zero(n);
+                else {
+                    return m_arith_util.is_zero(n);
+                }
             }
 
             bool is_times_minus_one(expr * n, expr * & arg) const {
@@ -1939,7 +1938,7 @@ namespace smt {
                 return m_bv_util.is_bv_sle(n);
             }
 
-            expr * mk_one(sort * s) {
+            expr * mk_one(sort * s) const {
                 return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s);
             }
 
@@ -1951,7 +1950,7 @@ namespace smt {
                 m_mutil.mk_add(t1, t2, r);
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
                 inv = false; // true if invert the sign
                 TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
                 if (is_var(lhs) && is_ground(rhs)) {
@@ -1986,12 +1985,12 @@ namespace smt {
                 return false;
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) {
                 bool inv;
                 return is_var_and_ground(lhs, rhs, v, t, inv);
             }
 
-            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const {
+            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
                 if (!is_app(n))
                     return false;
                 if (m_manager.is_eq(n))
@@ -2382,10 +2381,10 @@ namespace smt {
             quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s):
                 m_mf(mf),
                 m_manager(m),
-                m_mutil(m, s),
+                m_mutil(m),
                 m_array_util(m),
-                m_arith_util(m),
-                m_bv_util(m),
+                m_arith_util(m_mutil.get_arith_util()),
+                m_bv_util(m_mutil.get_bv_util()),
                 m_info(0) {
             }
 

From 799fb4a0d1e9b21a8af15759ecae4353dbb5d6bd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 21:26:09 +0100
Subject: [PATCH 06/10] Revert "Eliminated the dependency of the macro-finder
 on the simplifier."

This reverts commit 8310b24c521b6dac99a97a61ab74115c377db1b2.
---
 src/ast/macros/macro_finder.cpp   |  43 ++++++------
 src/ast/macros/macro_finder.h     |  17 +++--
 src/ast/macros/macro_manager.cpp  |   2 +-
 src/ast/macros/macro_util.cpp     | 106 ++++++++++++++++++------------
 src/ast/macros/macro_util.h       |  25 +++----
 src/ast/rewriter/arith_rewriter.h |  20 +++---
 src/ast/rewriter/poly_rewriter.h  |  57 ----------------
 src/smt/smt_model_finder.cpp      |  37 ++++++-----
 8 files changed, 139 insertions(+), 168 deletions(-)

diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index 604d10b04..285c0e5fb 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -21,9 +21,8 @@ Revision History:
 #include "ast/occurs.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
-#include "ast/rewriter/arith_rewriter.h"
 
-bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
+bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@@ -33,30 +32,30 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
 }
 
 /**
-   \brief Detect macros of the form
+   \brief Detect macros of the form 
    1- (forall (X) (= (+ (f X) (R X)) c))
    2- (forall (X) (<= (+ (f X) (R X)) c))
    3- (forall (X) (>= (+ (f X) (R X)) c))
 
    The second and third cases are first converted into
    (forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
-   and
+   and 
    (forall (X) (<= (k X) 0)) when case 2
    (forall (X) (>= (k X) 0)) when case 3
 
    For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
 */
-bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const {
+bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
-    arith_rewriter & arw = m_util.get_arith_rw();
-    arith_util & au = m_util.get_arith_util();
+    arith_simplifier_plugin * as = get_arith_simp();
+    arith_util & autil = as->get_arith_util();
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-
-    if (!au.is_le(body) && !au.is_ge(body) && !m_manager.is_eq(body))
+    
+    if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
         return false;
-    if (!au.is_add(to_app(body)->get_arg(0)))
+    if (!as->is_add(to_app(body)->get_arg(0)))
         return false;
     app_ref head(m_manager);
     expr_ref def(m_manager);
@@ -64,15 +63,15 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
         return false;
     app_ref new_body(m_manager);
-
+    
     if (!inv || m_manager.is_eq(body))
         new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
-    else if (au.is_le(body))
-        new_body = au.mk_ge(head, def);
+    else if (as->is_le(body))
+        new_body = autil.mk_ge(head, def);
     else
-        new_body = au.mk_le(head, def);
+        new_body = autil.mk_le(head, def);
 
-    quantifier_ref new_q(m_manager);
+    quantifier_ref new_q(m_manager); 
     new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
     proof * new_pr      = 0;
     if (m_manager.proofs_enabled()) {
@@ -83,16 +82,16 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
         return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
     }
     // is ge or le
-    //
+    // 
     TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
     func_decl * f   = head->get_decl();
     func_decl * k   = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app     = m_manager.mk_app(k, head->get_num_args(), head->get_args());
     expr_ref_buffer new_rhs_args(m_manager);
     expr_ref new_rhs2(m_manager);
-    arw.mk_add(def, k_app, new_rhs2);
+    as->mk_add(def, k_app, new_rhs2);
     expr * body1    = m_manager.mk_eq(head, new_rhs2);
-    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, au.mk_numeral(0, m_manager.get_sort(def)));
+    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(0)));
     quantifier * q1 = m_manager.update_quantifier(new_q, body1);
     expr * patterns[1] = { m_manager.mk_pattern(k_app) };
     quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2);
@@ -119,7 +118,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
    n is of the form: (forall (X) (iff (= (f X) t) def[X]))
 
    Convert it into:
-
+   
    (forall (X) (= (f X) (ite def[X] t (k X))))
    (forall (X) (not (= (k X) t)))
 
@@ -127,13 +126,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
 
    The new quantifiers and proofs are stored in new_exprs and new_prs
 */
-static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
+static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, 
                                          expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     func_decl * f = head->get_decl();
     func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app   = m.mk_app(k, head->get_num_args(), head->get_args());
     app * ite     = m.mk_ite(def, t, k_app);
-    app * body_1  = m.mk_eq(head, ite);
+    app * body_1  = m.mk_eq(head, ite); 
     app * body_2  = m.mk_not(m.mk_eq(k_app, t));
     quantifier * q1 = m.update_quantifier(q, body_1);
     expr * pats[1] = { m.mk_pattern(k_app) };
@@ -184,7 +183,7 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
             TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
             found_new_macro = true;
         }
-        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
+        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { 
             TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
             pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
             found_new_macro = true;
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 0c292eab8..7f1b27f0e 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -20,7 +20,8 @@ Revision History:
 #define MACRO_FINDER_H_
 
 #include "ast/macros/macro_manager.h"
-#include "ast/macros/macro_util.h"
+#include "ast/simplifier/arith_simplifier_plugin.h"
+
 
 bool is_macro_head(expr * n, unsigned num_decls);
 bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
@@ -33,15 +34,16 @@ inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app *
    as macros.
 */
 class macro_finder {
-    ast_manager &               m_manager;
+    ast_manager &               m_manager; 
     macro_manager &             m_macro_manager;
     macro_util &                m_util;
-
+    arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
     bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
-    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const;
-    bool is_macro(expr * n, app_ref & head, expr_ref & def) const;
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t) const;
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def) const;
+    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+
+    bool is_macro(expr * n, app_ref & head, expr_ref & def);
+    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
+    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
@@ -50,3 +52,4 @@ public:
 };
 
 #endif /* MACRO_FINDER_H_ */
+
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index f26a87445..bd330a2de 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -28,7 +28,7 @@ Revision History:
 macro_manager::macro_manager(ast_manager & m, simplifier & s):
     m_manager(m),
     m_simplifier(s),
-    m_util(m),
+    m_util(m, s),
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 415e77d03..35f2fbcfb 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -20,8 +20,8 @@ Revision History:
 #include "ast/macros/macro_util.h"
 #include "ast/occurs.h"
 #include "ast/ast_util.h"
-#include "ast/arith_decl_plugin.h"
-#include "ast/bv_decl_plugin.h"
+#include "ast/simplifier/arith_simplifier_plugin.h"
+#include "ast/simplifier/bv_simplifier_plugin.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -29,73 +29,96 @@ Revision History:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/bool_rewriter.h"
 
-macro_util::macro_util(ast_manager & m):
+macro_util::macro_util(ast_manager & m, simplifier & s):
     m_manager(m),
-    m_arith_rw(m),
-    m_arith_util(m_arith_rw.get_util()),
-    m_bv_rw(m),
-    m_bv_util(m_bv_rw.get_util()),
+    m_bv(m),
+    m_simplifier(s),
+    m_arith_simp(0),
+    m_bv_simp(0),
     m_forbidden_set(0),
     m_curr_clause(0) {
 }
 
+arith_simplifier_plugin * macro_util::get_arith_simp() const {
+    if (m_arith_simp == 0) {
+        const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
+    }
+    SASSERT(m_arith_simp != 0);
+    return m_arith_simp;
+}
+
+bv_simplifier_plugin * macro_util::get_bv_simp() const {
+    if (m_bv_simp == 0) {
+        const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("bv")));
+    }
+    SASSERT(m_bv_simp != 0);
+    return m_bv_simp;
+}
+
+
 bool macro_util::is_bv(expr * n) const {
-    return m_bv_util.is_bv(n);
+    return m_bv.is_bv(n);
 }
 
 bool macro_util::is_bv_sort(sort * s) const {
-    return m_bv_util.is_bv_sort(s);
+    return m_bv.is_bv_sort(s);
 }
 
 bool macro_util::is_add(expr * n) const {
-    return m_arith_util.is_add(n) || m_bv_util.is_bv_add(n);
+    return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n);
 }
 
 bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
-    return is_app(n) && to_app(n)->get_num_args() == 2 &&
-                ((m_arith_rw.is_mul(n) && m_arith_rw.is_times_minus_one(to_app(n)->get_arg(0), arg)) ||
-                 (m_bv_rw.is_mul(n) && m_bv_rw.is_times_minus_one(to_app(n)->get_arg(0), arg)));
+    return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg);
 }
 
 bool macro_util::is_le(expr * n) const {
-    return m_arith_util.is_le(n) || m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n);
+    return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
 }
 
 bool macro_util::is_le_ge(expr * n) const {
-    return m_arith_util.is_le(n) || m_arith_util.is_ge(n) ||
-           m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n);
+    return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+}
+
+poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const {
+    if (is_bv_sort(s))
+        return get_bv_simp();
+    else
+        return get_arith_simp();
 }
 
 app * macro_util::mk_zero(sort * s) const {
-    if (is_bv_sort(s))
-        return m_bv_util.mk_numeral(rational(0), s);
-    else
-        return m_arith_util.mk_numeral(0, s);
+    poly_simplifier_plugin * ps = get_poly_simp_for(s);
+    ps->set_curr_sort(s);
+    return ps->mk_zero();
 }
 
 void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
-    if (is_bv(t1))
-        r = m_bv_util.mk_bv_sub(t1, t2);
-    else
-        r = m_arith_util.mk_sub(t1, t2);
+    if (is_bv(t1)) {
+        r = m_bv.mk_bv_sub(t1, t2);
+    }
+    else {
+        get_arith_simp()->mk_sub(t1, t2, r);
+    }
 }
 
 void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
-    if (is_bv(t1))
-        r = m_bv_util.mk_bv_add(t1, t2);
-    else
-        m_arith_util.mk_add(t1, t2, r);
+    if (is_bv(t1)) {
+        r = m_bv.mk_bv_add(t1, t2);
+    }
+    else {
+        get_arith_simp()->mk_add(t1, t2, r);
+    }
 }
 
 void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const {
-    if (num_args == 0)
+    if (num_args == 0) {
         r = mk_zero(s);
-    else if (num_args == 1)
-        r = args[0];
-    else if (is_bv_sort(s))
-        m_bv_rw.mk_add(num_args, args, r);
-    else
-        m_arith_rw.mk_add(num_args, args, r);
+        return;
+    }
+    poly_simplifier_plugin * ps = get_poly_simp_for(s);
+    ps->set_curr_sort(s);
+    ps->mk_add(num_args, args, r);
 }
 
 /**
@@ -218,12 +241,13 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c
 
 bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const {
     // TODO: obsolete... we should move to collect_arith_macro_candidates
-    if (!m_manager.is_eq(n) && !m_arith_util.is_le(n) && !m_arith_util.is_ge(n))
+    arith_simplifier_plugin * as = get_arith_simp();
+    if (!m_manager.is_eq(n) && !as->is_le(n) && !as->is_ge(n))
         return false;
     expr * lhs = to_app(n)->get_arg(0);
     expr * rhs = to_app(n)->get_arg(1);
 
-    if (!m_arith_util.is_numeral(rhs))
+    if (!as->is_numeral(rhs))
         return false;
 
     inv = false;
@@ -248,7 +272,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
             !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
             h = arg;
         }
-        else if (h == 0 && m_arith_util.is_times_minus_one(arg, neg_arg) &&
+        else if (h == 0 && as->is_times_minus_one(arg, neg_arg) &&
                  is_macro_head(neg_arg, num_decls) &&
                  !is_forbidden(to_app(neg_arg)->get_decl()) &&
                  !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
@@ -263,11 +287,11 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
         return false;
     head = to_app(h);
     expr_ref tmp(m_manager);
-    m_arith_rw.mk_add(args.size(), args.c_ptr(), tmp);
+    as->mk_add(args.size(), args.c_ptr(), tmp);
     if (inv)
-        m_arith_rw.mk_sub(tmp, rhs, def);
+        as->mk_sub(tmp, rhs, def);
     else
-        m_arith_rw.mk_sub(rhs, tmp, def);
+        as->mk_sub(rhs, tmp, def);
     return true;
 }
 
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index 3da8accc9..d76f2f0d3 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -22,8 +22,12 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/obj_hashtable.h"
-#include "ast/rewriter/arith_rewriter.h"
-#include "ast/rewriter/bv_rewriter.h"
+#include "ast/simplifier/simplifier.h"
+
+class poly_simplifier_plugin;
+class arith_simplifier_plugin;
+class bv_simplifier_plugin;
+class basic_simplifier_plugin;
 
 class macro_util {
 public:
@@ -58,10 +62,10 @@ public:
 
 private:
     ast_manager &               m_manager;
-    mutable arith_rewriter      m_arith_rw;
-    arith_util &                m_arith_util;
-    mutable bv_rewriter         m_bv_rw;
-    bv_util &                   m_bv_util;
+    bv_util                     m_bv;
+    simplifier &                m_simplifier;
+    arith_simplifier_plugin *   m_arith_simp;
+    bv_simplifier_plugin    *   m_bv_simp;
     obj_hashtable<func_decl> *  m_forbidden_set;
 
     bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@@ -90,13 +94,11 @@ private:
 
 
 public:
-    macro_util(ast_manager & m);
+    macro_util(ast_manager & m, simplifier & s);
     void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; }
 
-    arith_util & get_arith_util() const { return m_arith_util; }
-    bv_util & get_bv_util() const { return m_bv_util; }
-    arith_rewriter & get_arith_rw() const { return m_arith_rw; }
-    bv_rewriter & get_bv_rw() const { return m_bv_rw; }
+    arith_simplifier_plugin * get_arith_simp() const;
+    bv_simplifier_plugin * get_bv_simp() const;
 
     bool is_macro_head(expr * n, unsigned num_decls) const;
     bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
@@ -135,6 +137,7 @@ public:
     void mk_sub(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const;
+    poly_simplifier_plugin * get_poly_simp_for(sort * s) const;
 };
 
 #endif
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 2342782c1..de849dbd7 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -29,10 +29,10 @@ protected:
     bool        m_expand_power;
     bool        m_mul2power;
     bool        m_expand_tan;
-
+    
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
-
+    
     bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
     bool is_zero(expr * n) const { return m_util.is_zero(n); }
@@ -77,7 +77,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result);
-
+    
     bool is_reduce_power_target(expr * arg, bool is_eq);
     expr * reduce_power(expr * arg, bool is_eq);
     br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
@@ -154,16 +154,16 @@ public:
         if (mk_rem_core(arg1, arg2, result) == BR_FAILED)
             result = m().mk_app(get_fid(), OP_REM, arg1, arg2);
     }
-
+    
     br_status mk_to_int_core(expr * arg, expr_ref & result);
     br_status mk_to_real_core(expr * arg, expr_ref & result);
-    void mk_to_int(expr * arg, expr_ref & result) {
+    void mk_to_int(expr * arg, expr_ref & result) { 
         if (mk_to_int_core(arg, result) == BR_FAILED)
-            result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg);
+            result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); 
     }
-    void mk_to_real(expr * arg, expr_ref & result) {
-        if (mk_to_real_core(arg, result) == BR_FAILED)
-            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg);
+    void mk_to_real(expr * arg, expr_ref & result) { 
+        if (mk_to_real_core(arg, result) == BR_FAILED)  
+            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); 
     }
     br_status mk_is_int(expr * arg, expr_ref & result);
 
@@ -178,8 +178,6 @@ public:
     br_status mk_sinh_core(expr * arg, expr_ref & result);
     br_status mk_cosh_core(expr * arg, expr_ref & result);
     br_status mk_tanh_core(expr * arg, expr_ref & result);
-
-    arith_util & get_util() { return m_util; }
 };
 
 #endif
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 81c5ea132..5d38e4b10 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -159,63 +159,6 @@ public:
         expr* args[2] = { a1, a2 };
         mk_sub(2, args, result);
     }
-
-    bool is_times_minus_one(expr * n, expr * & r) const {
-        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
-            r = to_app(n)->get_arg(1);
-            return true;
-        }
-        return false;
-    }
-
-    /**
-    \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
-    \c inv = true will contain true if (- v) is found, and false otherwise.
-    */
-    bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
-        if (!is_add(n) || is_ground(n))
-            return false;
-
-        ptr_buffer<expr> args;
-        v = 0;
-        expr * curr = to_app(n);
-        bool stop = false;
-        inv = false;
-        while (!stop) {
-            expr * arg;
-            expr * neg_arg;
-            if (is_add(curr)) {
-                arg = to_app(curr)->get_arg(0);
-                curr = to_app(curr)->get_arg(1);
-            }
-            else {
-                arg = curr;
-                stop = true;
-            }
-            if (is_ground(arg)) {
-                args.push_back(arg);
-            }
-            else if (is_var(arg)) {
-                if (v != 0)
-                    return false; // already found variable
-                v = to_var(arg);
-            }
-            else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
-                if (v != 0)
-                    return false; // already found variable
-                v = to_var(neg_arg);
-                inv = true;
-            }
-            else {
-                return false; // non ground term.
-            }
-        }
-        if (v == 0)
-            return false; // did not find variable
-        SASSERT(!args.empty());
-        mk_add(args.size(), args.c_ptr(), t);
-        return true;
-    }
 };
 
 
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 0a80460f5..94a6a7267 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1873,12 +1873,12 @@ namespace smt {
            fill the structure quantifier_info.
         */
         class quantifier_analyzer {
-            model_finder &       m_mf;
+            model_finder&        m_mf;
             ast_manager &        m_manager;
             macro_util           m_mutil;
             array_util           m_array_util;
-            arith_util &         m_arith_util;
-            bv_util &            m_bv_util;
+            arith_util           m_arith_util;
+            bv_util              m_bv_util;
 
             quantifier_info *    m_info;
 
@@ -1897,12 +1897,14 @@ namespace smt {
                 m_info->insert_qinfo(qi);
             }
 
+            arith_simplifier_plugin * get_arith_simp() const { return m_mutil.get_arith_simp(); }
+            bv_simplifier_plugin * get_bv_simp() const { return m_mutil.get_bv_simp(); }
+
             bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) const {
-                return m_mutil.get_arith_rw().is_var_plus_ground(n, inv, v, t) ||
-                       m_mutil.get_bv_rw().is_var_plus_ground(n, inv, v, t);
+                return get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t);
             }
 
-            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) const {
+            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
                 bool inv;
                 TRACE("is_var_plus_ground", tout << mk_pp(n, m_manager) << "\n";
                       tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n";
@@ -1915,11 +1917,10 @@ namespace smt {
             }
 
             bool is_zero(expr * n) const {
-                if (m_bv_util.is_bv(n))
-                    return m_bv_util.is_zero(n);
-                else {
-                    return m_arith_util.is_zero(n);
-                }
+                if (get_bv_simp()->is_bv(n))
+                    return get_bv_simp()->is_zero_safe(n);
+                else
+                    return get_arith_simp()->is_zero_safe(n);
             }
 
             bool is_times_minus_one(expr * n, expr * & arg) const {
@@ -1938,7 +1939,7 @@ namespace smt {
                 return m_bv_util.is_bv_sle(n);
             }
 
-            expr * mk_one(sort * s) const {
+            expr * mk_one(sort * s) {
                 return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s);
             }
 
@@ -1950,7 +1951,7 @@ namespace smt {
                 m_mutil.mk_add(t1, t2, r);
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const {
                 inv = false; // true if invert the sign
                 TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
                 if (is_var(lhs) && is_ground(rhs)) {
@@ -1985,12 +1986,12 @@ namespace smt {
                 return false;
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const {
                 bool inv;
                 return is_var_and_ground(lhs, rhs, v, t, inv);
             }
 
-            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
+            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const {
                 if (!is_app(n))
                     return false;
                 if (m_manager.is_eq(n))
@@ -2381,10 +2382,10 @@ namespace smt {
             quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s):
                 m_mf(mf),
                 m_manager(m),
-                m_mutil(m),
+                m_mutil(m, s),
                 m_array_util(m),
-                m_arith_util(m_mutil.get_arith_util()),
-                m_bv_util(m_mutil.get_bv_util()),
+                m_arith_util(m),
+                m_bv_util(m),
                 m_info(0) {
             }
 

From 36dd2b653035532a253fbb85d507fac52418af3a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 25 Aug 2017 15:01:54 +0100
Subject: [PATCH 07/10] Re-enabled macro-related options for the smt_context

---
 src/smt/params/preprocessor_params.cpp | 2 ++
 src/smt/params/smt_params_helper.pyg   | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 9267dbeba..679cd0f39 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -22,6 +22,8 @@ Revision History:
 void preprocessor_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_macro_finder            = p.macro_finder();
+    m_quasi_macros            = p.quasi_macros();
+    m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
     m_refine_inj_axiom        = p.refine_inj_axioms();
 }
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 5b5c7328c..d6ca8c9b2 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -7,6 +7,8 @@ def_module_params(module_name='smt',
                           ('random_seed', UINT, 0, 'random seed for the smt solver'),
                           ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
                           ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
+                          ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
+                          ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),

From 3e0926fb822195f33e9b585b0aac93094b9a58b5 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 25 Aug 2017 15:23:25 +0100
Subject: [PATCH 08/10] Whitespace

---
 src/ast/macros/quasi_macros.cpp | 74 ++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 37 deletions(-)

diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index b39adde03..97ab55bd4 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -31,7 +31,7 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s)
   m_new_qsorts(m) {
 }
 
-quasi_macros::~quasi_macros() {    
+quasi_macros::~quasi_macros() {
 }
 
 void quasi_macros::find_occurrences(expr * e) {
@@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
 
     // we remember whether we have seen an expr once, or more than once;
     // when we see it the second time, we don't have to visit it another time,
-    // as we are only interested in finding unique function applications. 
+    // as we are only interested in finding unique function applications.
     m_visited_once.reset();
     m_visited_more.reset();
 
@@ -64,8 +64,8 @@ void quasi_macros::find_occurrences(expr * e) {
                 if (is_non_ground_uninterp(cur)) {
                     func_decl * f = to_app(cur)->get_decl();
                     m_occurrences.insert_if_not_there(f, 0);
-                    occurrences_map::iterator it = m_occurrences.find_iterator(f);                    
-                    it->m_value++;                    
+                    occurrences_map::iterator it = m_occurrences.find_iterator(f);
+                    it->m_value++;
                 }
                 j = to_app(cur)->get_num_args();
                 while (j)
@@ -84,16 +84,16 @@ bool quasi_macros::is_unique(func_decl * f) const {
     return m_occurrences.find(f) == 1;
 }
 
-struct var_dep_proc {    
+struct var_dep_proc {
     bit_vector m_bitset;
 public:
     var_dep_proc(quantifier * q) { m_bitset.resize(q->get_num_decls(), false); }
     void operator()(var * n) { m_bitset.set(n->get_idx(), true); }
     void operator()(quantifier * n) {}
     void operator()(app * n) {}
-    bool all_used(void) { 
+    bool all_used(void) {
         for (unsigned i = 0; i < m_bitset.size() ; i++)
-            if (!m_bitset.get(i)) 
+            if (!m_bitset.get(i))
                 return false;
         return true;
     }
@@ -101,7 +101,7 @@ public:
 
 bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
     // CMW: This checks whether all variables in q are used _somewhere_ deep down in the children of a
-    
+
     /* var_dep_proc proc(q);
     for_each_expr(proc, a);
     return proc.all_used(); */
@@ -116,14 +116,14 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
     }
 
     for (unsigned i = 0; i < bitset.size() ; i++) {
-        if (!bitset.get(i)) 
+        if (!bitset.get(i))
             return false;
     }
 
     return true;
 }
 
-bool quasi_macros::depends_on(expr * e, func_decl * f) const { 
+bool quasi_macros::depends_on(expr * e, func_decl * f) const {
     ptr_vector<expr> todo;
     expr_mark visited;
     todo.push_back(e);
@@ -133,12 +133,12 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
 
         if (visited.is_marked(cur))
             continue;
-        
+
         if (is_app(cur)) {
             app * a = to_app(cur);
-            if (a->get_decl() == f) 
+            if (a->get_decl() == f)
                 return true;
-            
+
             unsigned j = a->get_num_args();
             while (j>0)
                 todo.push_back(a->get_arg(--j));
@@ -151,7 +151,7 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
 
 bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
     // Our definition of a quasi-macro:
-    // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, 
+    // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
     // f[X] contains all universally quantified variables, and f does not occur in T[X].
     TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
 
@@ -165,14 +165,14 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
             if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
                 !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
                 a = to_app(lhs);
-                t = rhs;                
+                t = rhs;
                 return true;
             } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
-                !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {                
+                !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
                 a = to_app(rhs);
-                t = lhs;                
+                t = lhs;
                 return true;
-            }            
+            }
         } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
                    is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
             a = to_app(to_app(qe)->get_arg(0));
@@ -189,7 +189,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
 }
 
 void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro) {
-    m_new_var_names.reset();    
+    m_new_var_names.reset();
     m_new_vars.reset();
     m_new_qsorts.reset();
     m_new_eqs.reset();
@@ -197,19 +197,19 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
     func_decl * f = a->get_decl();
 
     // CMW: we rely on the fact that all variables in q appear at least once as
-    // a direct argument of `a'. 
+    // a direct argument of `a'.
 
     bit_vector v_seen;
-    v_seen.resize(q->get_num_decls(), false);    
+    v_seen.resize(q->get_num_decls(), false);
     for (unsigned i = 0 ; i < a->get_num_args() ; i++) {
-        if (!is_var(a->get_arg(i)) || 
+        if (!is_var(a->get_arg(i)) ||
             v_seen.get(to_var(a->get_arg(i))->get_idx())) {
             unsigned inx = m_new_var_names.size();
             m_new_name.str("");
             m_new_name << "X" << inx;
-            m_new_var_names.push_back(symbol(m_new_name.str().c_str()));            
+            m_new_var_names.push_back(symbol(m_new_name.str().c_str()));
             m_new_qsorts.push_back(f->get_domain()[i]);
-           
+
             m_new_vars.push_back(m_manager.mk_var(inx + q->get_num_decls(), f->get_domain()[i]));
             m_new_eqs.push_back(m_manager.mk_eq(m_new_vars.back(), a->get_arg(i)));
         } else {
@@ -228,13 +228,13 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
         new_var_names_rev.push_back(m_new_var_names.get(i));
         new_qsorts_rev.push_back(m_new_qsorts.get(i));
     }
-    
+
     // We want to keep all the old variables [already reversed]
     for (unsigned i = 0 ; i < q->get_num_decls() ; i++) {
         new_var_names_rev.push_back(q->get_decl_name(i));
         new_qsorts_rev.push_back(q->get_decl_sort(i));
     }
-    
+
     // Macro  :=  Forall m_new_vars . appl = ITE( m_new_eqs, t, f_else)
 
     app_ref appl(m_manager);
@@ -251,28 +251,28 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
 
     eq = m_manager.mk_eq(appl, ite);
 
-    macro = m_manager.mk_quantifier(true, new_var_names_rev.size(), 
+    macro = m_manager.mk_quantifier(true, new_var_names_rev.size(),
                                     new_qsorts_rev.c_ptr(), new_var_names_rev.c_ptr(), eq);
 }
 
 bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
-                          for (unsigned i = 0 ; i < n ; i++) 
+                          for (unsigned i = 0 ; i < n ; i++)
                               tout << i << ": " << mk_pp(exprs[i], m_manager) << std::endl; );
     bool res = false;
     m_occurrences.reset();
-    
 
-    // Find out how many non-ground appearences for each uninterpreted function there are    
+
+    // Find out how many non-ground appearences for each uninterpreted function there are
     for ( unsigned i = 0 ; i < n ; i++ )
         find_occurrences(exprs[i]);
 
     TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
-    for (occurrences_map::iterator it = m_occurrences.begin(); 
-         it != m_occurrences.end(); 
+    for (occurrences_map::iterator it = m_occurrences.begin();
+         it != m_occurrences.end();
          it++)
         tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
-   
+
     // Find all macros
     for ( unsigned i = 0 ; i < n ; i++ ) {
         app_ref a(m_manager);
@@ -293,7 +293,7 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     return res;
 }
 
-void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {     
+void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     for ( unsigned i = 0 ; i < n ; i++ ) {
         expr_ref r(m_manager), rs(m_manager);
         proof_ref pr(m_manager), ps(m_manager);
@@ -301,7 +301,7 @@ void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const
         m_macro_manager.expand_macros(exprs[i], p, r, pr);
         m_simplifier(r, rs, ps);
         new_exprs.push_back(rs);
-        new_prs.push_back(ps);    
+        new_prs.push_back(ps);
     }
 }
 
@@ -313,9 +313,9 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const *
         // just copy them over
         for ( unsigned i = 0 ; i < n ; i++ ) {
             new_exprs.push_back(exprs[i]);
-            if (m_manager.proofs_enabled()) 
+            if (m_manager.proofs_enabled())
                 new_prs.push_back(prs[i]);
         }
         return false;
-    }    
+    }
 }

From 31496b662548844350d1468d5a7e51502131589b Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 25 Aug 2017 15:29:29 +0100
Subject: [PATCH 09/10] Whitespace

---
 src/ast/macros/quasi_macros.h | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 3a9b6074e..849fe8bce 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -34,22 +34,22 @@ class quasi_macros {
     macro_manager &           m_macro_manager;
     simplifier &              m_simplifier;
     occurrences_map           m_occurrences;
-    ptr_vector<expr>          m_todo;    
+    ptr_vector<expr>          m_todo;
 
     vector<symbol>            m_new_var_names;
     expr_ref_vector           m_new_vars;
     expr_ref_vector           m_new_eqs;
     sort_ref_vector           m_new_qsorts;
-    std::stringstream         m_new_name;    
+    std::stringstream         m_new_name;
     expr_mark                 m_visited_once;
     expr_mark                 m_visited_more;
-    
+
     bool is_unique(func_decl * f) const;
     bool is_non_ground_uninterp(expr const * e) const;
-    bool fully_depends_on(app * a, quantifier * q) const;    
+    bool fully_depends_on(app * a, quantifier * q) const;
     bool depends_on(expr * e, func_decl * f) const;
 
-    bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const;        
+    bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const;
     void quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro);
 
     void find_occurrences(expr * e);
@@ -59,11 +59,11 @@ class quasi_macros {
 public:
     quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
     ~quasi_macros();
-    
+
     /**
        \brief Find pure function macros and apply them.
     */
-    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);    
+    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 };
 
 #endif

From b8a81bcb09e59890ac8ebc2a9f253cc610c97129 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 25 Aug 2017 20:21:57 +0100
Subject: [PATCH 10/10] Added unsat core support to the macro-finder.

---
 src/ast/macros/macro_finder.cpp         | 59 +++++++++++++--------
 src/ast/macros/macro_finder.h           | 17 ++----
 src/ast/macros/macro_manager.cpp        | 26 +++++++--
 src/ast/macros/macro_manager.h          |  7 ++-
 src/ast/macros/quasi_macros.cpp         | 29 +++++-----
 src/ast/macros/quasi_macros.h           |  4 +-
 src/smt/asserted_formulas.cpp           | 70 ++++++++++++++-----------
 src/smt/asserted_formulas.h             | 14 +++--
 src/smt/smt_context.h                   |  4 +-
 src/tactic/ufbv/macro_finder_tactic.cpp | 12 +++--
 src/tactic/ufbv/quasi_macros_tactic.cpp | 52 ++++++++++--------
 11 files changed, 169 insertions(+), 125 deletions(-)

diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index 285c0e5fb..90e64fb0a 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -32,27 +32,27 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
 }
 
 /**
-   \brief Detect macros of the form 
+   \brief Detect macros of the form
    1- (forall (X) (= (+ (f X) (R X)) c))
    2- (forall (X) (<= (+ (f X) (R X)) c))
    3- (forall (X) (>= (+ (f X) (R X)) c))
 
    The second and third cases are first converted into
    (forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
-   and 
+   and
    (forall (X) (<= (k X) 0)) when case 2
    (forall (X) (>= (k X) 0)) when case 3
 
    For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
 */
-bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     arith_simplifier_plugin * as = get_arith_simp();
     arith_util & autil = as->get_arith_util();
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-    
+
     if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
         return false;
     if (!as->is_add(to_app(body)->get_arg(0)))
@@ -63,7 +63,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
         return false;
     app_ref new_body(m_manager);
-    
+
     if (!inv || m_manager.is_eq(body))
         new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
     else if (as->is_le(body))
@@ -71,18 +71,19 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     else
         new_body = autil.mk_le(head, def);
 
-    quantifier_ref new_q(m_manager); 
+    quantifier_ref new_q(m_manager);
     new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
     proof * new_pr      = 0;
     if (m_manager.proofs_enabled()) {
         proof * rw  = m_manager.mk_rewrite(n, new_q);
         new_pr      = m_manager.mk_modus_ponens(pr, rw);
     }
+    expr_dependency * new_dep = dep;
     if (m_manager.is_eq(body)) {
-        return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
+        return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep);
     }
     // is ge or le
-    // 
+    //
     TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
     func_decl * f   = head->get_decl();
     func_decl * k   = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
@@ -111,6 +112,10 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
         new_prs.push_back(pr1);
         new_prs.push_back(pr2);
     }
+    if (dep) {
+        new_deps.push_back(new_dep);
+        new_deps.push_back(new_dep);
+    }
     return true;
 }
 
@@ -118,7 +123,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
    n is of the form: (forall (X) (iff (= (f X) t) def[X]))
 
    Convert it into:
-   
+
    (forall (X) (= (f X) (ite def[X] t (k X))))
    (forall (X) (not (= (k X) t)))
 
@@ -126,13 +131,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
 
    The new quantifiers and proofs are stored in new_exprs and new_prs
 */
-static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, 
-                                         expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_dependency * dep,
+                                         expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) {
     func_decl * f = head->get_decl();
     func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app   = m.mk_app(k, head->get_num_args(), head->get_args());
     app * ite     = m.mk_ite(def, t, k_app);
-    app * body_1  = m.mk_eq(head, ite); 
+    app * body_1  = m.mk_eq(head, ite);
     app * body_2  = m.mk_not(m.mk_eq(k_app, t));
     quantifier * q1 = m.update_quantifier(q, body_1);
     expr * pats[1] = { m.mk_pattern(k_app) };
@@ -153,6 +158,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
         new_prs.push_back(pr1);
         new_prs.push_back(pr2);
     }
+    new_deps.push_back(dep);
+    new_deps.push_back(dep);
 }
 
 macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
@@ -164,57 +171,67 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
 macro_finder::~macro_finder() {
 }
 
-bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps,  expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "starting expand_macros:\n";
           m_macro_manager.display(tout););
     bool found_new_macro = false;
     for (unsigned i = 0; i < num; i++) {
         expr * n       = exprs[i];
         proof * pr     = m_manager.proofs_enabled() ? prs[i] : 0;
+        expr_dependency * depi = deps != 0 ? deps[i] : 0;
         expr_ref new_n(m_manager), def(m_manager);
         proof_ref new_pr(m_manager);
-        m_macro_manager.expand_macros(n, pr, new_n, new_pr);
+        expr_dependency_ref new_dep(m_manager);
+        m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep);
         app_ref head(m_manager), t(m_manager);
-        if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
+        if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
             TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
             found_new_macro = true;
         }
-        else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) {
+        else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) {
             TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
             found_new_macro = true;
         }
-        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { 
+        else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
             TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
-            pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
+            pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps);
             found_new_macro = true;
         }
         else {
             new_exprs.push_back(new_n);
             if (m_manager.proofs_enabled())
                 new_prs.push_back(new_pr);
+            if (deps != 0)
+                new_deps.push_back(new_dep);
         }
     }
     return found_new_macro;
 }
 
-void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "processing macros...\n";);
     expr_ref_vector   _new_exprs(m_manager);
     proof_ref_vector  _new_prs(m_manager);
-    if (expand_macros(num, exprs, prs, _new_exprs, _new_prs)) {
+    expr_dependency_ref_vector _new_deps(m_manager);
+    if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
         while (true) {
             expr_ref_vector  old_exprs(m_manager);
             proof_ref_vector old_prs(m_manager);
+            expr_dependency_ref_vector old_deps(m_manager);
             _new_exprs.swap(old_exprs);
             _new_prs.swap(old_prs);
+            _new_deps.swap(old_deps);
             SASSERT(_new_exprs.empty());
             SASSERT(_new_prs.empty());
-            if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), _new_exprs, _new_prs))
+            SASSERT(_new_deps.empty());
+            if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(),
+                               _new_exprs, _new_prs, _new_deps))
                 break;
         }
     }
     new_exprs.append(_new_exprs);
     new_prs.append(_new_prs);
+    new_deps.append(_new_deps);
 }
 
 
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 7f1b27f0e..996d613e8 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -23,32 +23,23 @@ Revision History:
 #include "ast/simplifier/arith_simplifier_plugin.h"
 
 
-bool is_macro_head(expr * n, unsigned num_decls);
-bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
-inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app * & head, expr * & def) {
-    return is_simple_macro(m, n, num_decls, 0, head, def);
-}
-
 /**
    \brief Macro finder is responsible for finding universally quantified sub-formulas that can be used
    as macros.
 */
 class macro_finder {
-    ast_manager &               m_manager; 
+    ast_manager &               m_manager;
     macro_manager &             m_macro_manager;
     macro_util &                m_util;
     arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
-    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
-    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
-
+    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
+    bool is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
     bool is_macro(expr * n, app_ref & head, expr_ref & def);
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
     ~macro_finder();
-    void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 };
 
 #endif /* MACRO_FINDER_H_ */
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index bd330a2de..0f16545d4 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -25,13 +25,14 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/recurse_expr_def.h"
 
-macro_manager::macro_manager(ast_manager & m, simplifier & s):
+macro_manager::macro_manager(ast_manager & m, simplifier & s) :
     m_manager(m),
     m_simplifier(s),
     m_util(m, s),
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),
+    m_macro_deps(m),
     m_forbidden(m),
     m_deps(m) {
     m_util.set_forbidden_set(&m_forbidden_set);
@@ -60,13 +61,16 @@ void macro_manager::restore_decls(unsigned old_sz) {
     for (unsigned i = old_sz; i < sz; i++) {
         m_decl2macro.erase(m_decls.get(i));
         m_deps.erase(m_decls.get(i));
-        if (m_manager.proofs_enabled())
+        if (m_manager.proofs_enabled()) {
             m_decl2macro_pr.erase(m_decls.get(i));
+            m_decl2macro_dep.erase(m_decls.get(i));
+        }
     }
     m_decls.shrink(old_sz);
     m_macros.shrink(old_sz);
     if (m_manager.proofs_enabled())
         m_macro_prs.shrink(old_sz);
+    m_macro_deps.shrink(old_sz);
 }
 
 void macro_manager::restore_forbidden(unsigned old_sz) {
@@ -79,16 +83,18 @@ void macro_manager::restore_forbidden(unsigned old_sz) {
 void macro_manager::reset() {
     m_decl2macro.reset();
     m_decl2macro_pr.reset();
+    m_decl2macro_dep.reset();
     m_decls.reset();
     m_macros.reset();
     m_macro_prs.reset();
+    m_macro_deps.reset();
     m_scopes.reset();
     m_forbidden_set.reset();
     m_forbidden.reset();
     m_deps.reset();
 }
 
-bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
+bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) {
     TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(m, m_manager) << "\n";);
 
     // if we already have a macro for f then return false;
@@ -115,6 +121,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
         m_macro_prs.push_back(pr);
         m_decl2macro_pr.insert(f, pr);
     }
+    m_macro_deps.push_back(dep);
+    m_decl2macro_dep.insert(f, dep);
 
     TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
 
@@ -195,7 +203,8 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
 
 macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm, simplifier & s):
     simplifier(m),
-    m_macro_manager(mm) {
+    m_macro_manager(mm),
+    m_used_macro_dependencies(m) {
     // REMARK: theory simplifier should not be used by macro_expander...
     // is_arith_macro rewrites a quantifer such as:
     //   forall (x Int) (= (+ x (+ (f x) 1)) 2)
@@ -286,34 +295,41 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
         }
         else {
             p = 0;
+            expr_dependency * ed = m_macro_manager.m_decl2macro_dep.find(d);
+            m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed);
         }
         return true;
     }
     return false;
 }
 
-void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) {
+void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep) {
     if (has_macros()) {
         // Expand macros with "real" proof production support (NO rewrite*)
         expr_ref old_n(m_manager);
         proof_ref old_pr(m_manager);
+        expr_dependency_ref old_dep(m_manager);
         old_n  = n;
         old_pr = pr;
+        old_dep = dep;
         for (;;) {
             macro_expander proc(m_manager, *this, m_simplifier);
             proof_ref n_eq_r_pr(m_manager);
             TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m_manager) << "\n";);
             proc(old_n, r, n_eq_r_pr);
             new_pr = m_manager.mk_modus_ponens(old_pr, n_eq_r_pr);
+            new_dep = m_manager.mk_join(old_dep, proc.m_used_macro_dependencies);
             if (r.get() == old_n.get())
                 return;
             old_n  = r;
             old_pr = new_pr;
+            old_dep = new_dep;
         }
     }
     else {
         r      = n;
         new_pr = pr;
+        new_dep = dep;
     }
 }
 
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index b72c1e6bf..111027f73 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -42,9 +42,11 @@ class macro_manager {
 
     obj_map<func_decl, quantifier *> m_decl2macro;    // func-decl -> quantifier
     obj_map<func_decl, proof *>      m_decl2macro_pr; // func-decl -> quantifier_proof
+    obj_map<func_decl, expr_dependency *> m_decl2macro_dep; // func-decl -> unsat core dependency
     func_decl_ref_vector             m_decls;
     quantifier_ref_vector            m_macros;
     proof_ref_vector                 m_macro_prs;
+    expr_dependency_ref_vector       m_macro_deps;
     obj_hashtable<func_decl>         m_forbidden_set;
     func_decl_ref_vector             m_forbidden;
     struct scope {
@@ -64,6 +66,7 @@ class macro_manager {
         virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
         virtual void reduce1_quantifier(quantifier * q);
     public:
+        expr_dependency_ref m_used_macro_dependencies;
         macro_expander(ast_manager & m, macro_manager & mm, simplifier & s);
         ~macro_expander();
     };
@@ -74,7 +77,7 @@ public:
     ~macro_manager();
     ast_manager & get_manager() const { return m_manager; }
     macro_util & get_util() { return m_util; }
-    bool insert(func_decl * f, quantifier * m, proof * pr);
+    bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep);
     bool has_macros() const { return !m_macros.empty(); }
     void push_scope();
     void pop_scope(unsigned num_scopes);
@@ -90,7 +93,7 @@ public:
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; }
     void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
-    void expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr);
+    void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
 
 
 };
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index 97ab55bd4..6206d0311 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -264,17 +264,16 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
 
 
     // Find out how many non-ground appearences for each uninterpreted function there are
-    for ( unsigned i = 0 ; i < n ; i++ )
+    for (unsigned i = 0 ; i < n ; i++)
         find_occurrences(exprs[i]);
 
-    TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
-    for (occurrences_map::iterator it = m_occurrences.begin();
-         it != m_occurrences.end();
-         it++)
-        tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
+    TRACE("quasi_macros",
+        tout << "Occurrences: " << std::endl;
+        for (auto & kd : m_occurrences)
+            tout << kd.m_key->get_name() << ": " << kd.m_value << std::endl; );
 
     // Find all macros
-    for ( unsigned i = 0 ; i < n ; i++ ) {
+    for (unsigned i = 0 ; i < n ; i++) {
         app_ref a(m_manager);
         expr_ref t(m_manager);
         if (is_quasi_macro(exprs[i], a, t)) {
@@ -285,7 +284,8 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
             proof * pr = 0;
             if (m_manager.proofs_enabled())
                 pr = m_manager.mk_def_axiom(macro);
-            if (m_macro_manager.insert(a->get_decl(), macro, pr))
+            expr_dependency * dep = 0;
+            if (m_macro_manager.insert(a->get_decl(), macro, pr, dep))
                 res = true;
         }
     }
@@ -293,21 +293,24 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     return res;
 }
 
-void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
-    for ( unsigned i = 0 ; i < n ; i++ ) {
+void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
+    for (unsigned i = 0 ; i < n ; i++) {
         expr_ref r(m_manager), rs(m_manager);
         proof_ref pr(m_manager), ps(m_manager);
         proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
-        m_macro_manager.expand_macros(exprs[i], p, r, pr);
+        expr_dependency * dep = deps[i];
+        expr_dependency_ref new_dep(m_manager);
+        m_macro_manager.expand_macros(exprs[i], p, dep, r, pr, new_dep);
         m_simplifier(r, rs, ps);
         new_exprs.push_back(rs);
         new_prs.push_back(ps);
+        new_deps.push_back(new_dep);
     }
 }
 
-bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     if (find_macros(n, exprs)) {
-        apply_macros(n, exprs, prs, new_exprs, new_prs);
+        apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps);
         return true;
     } else {
         // just copy them over
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 849fe8bce..50fa04af4 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -54,7 +54,7 @@ class quasi_macros {
 
     void find_occurrences(expr * e);
     bool find_macros(unsigned n, expr * const * exprs);
-    void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 
 public:
     quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
@@ -63,7 +63,7 @@ public:
     /**
        \brief Find pure function macros and apply them.
     */
-    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 };
 
 #endif
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index cbbb9a6bc..dabae9fbd 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -75,7 +75,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
 void asserted_formulas::setup() {
     switch (m_params.m_lift_ite) {
     case LI_FULL:
-        m_params.m_ng_lift_ite = LI_NONE; 
+        m_params.m_ng_lift_ite = LI_NONE;
         break;
     case LI_CONSERVATIVE:
         if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
@@ -84,7 +84,7 @@ void asserted_formulas::setup() {
     default:
         break;
     }
- 
+
     if (m_params.m_relevancy_lvl == 0)
         m_params.m_relevancy_lemma = false;
 }
@@ -97,7 +97,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie
     s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params));
     bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params);
     s.register_plugin(bvsimp);
-    s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));    
+    s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));
     s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp));
     s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp));
 }
@@ -140,7 +140,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
 
 
 void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
-    if (inconsistent()) 
+    if (inconsistent())
         return;
     if (!m_params.m_preprocess) {
         push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs);
@@ -175,7 +175,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
 }
 
 void asserted_formulas::assert_expr(expr * e) {
-    if (inconsistent()) 
+    if (inconsistent())
         return;
     assert_expr(e, m.mk_asserted(e));
 }
@@ -197,7 +197,7 @@ void asserted_formulas::push_scope() {
     m_bv_sharing.push_scope();
     commit();
 }
- 
+
 void asserted_formulas::pop_scope(unsigned num_scopes) {
     TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
     m_bv_sharing.pop_scope(num_scopes);
@@ -228,15 +228,15 @@ void asserted_formulas::reset() {
 
 #ifdef Z3DEBUG
 bool asserted_formulas::check_well_sorted() const {
-    for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { 
-        if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; 
+    for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
+        if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false;
     }
     return true;
 }
 #endif
 
 void asserted_formulas::reduce() {
-    if (inconsistent()) 
+    if (inconsistent())
         return;
     if (canceled()) {
         return;
@@ -253,7 +253,7 @@ void asserted_formulas::reduce() {
 
 
 #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); }  TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return;  }
-    
+
     set_eliminate_and(false); // do not eliminate and before nnf.
     INVOKE(m_params.m_propagate_booleans, propagate_booleans());
     INVOKE(m_params.m_propagate_values, propagate_values());
@@ -266,18 +266,18 @@ void asserted_formulas::reduce() {
     INVOKE(m_params.m_lift_ite != LI_NONE, lift_ite());
     INVOKE(m_params.m_eliminate_term_ite && m_params.m_lift_ite != LI_FULL, eliminate_term_ite());
     INVOKE(m_params.m_refine_inj_axiom && has_quantifiers(), refine_inj_axiom());
-    INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall());    
-    TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout););    
+    INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall());
+    TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout););
     INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
-    INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());    
+    INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
     INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
     INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
     INVOKE(m_params.m_ematching && has_quantifiers(), infer_patterns());
     INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
     INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
-    // temporary HACK: make sure that arith & bv are list-assoc 
+    // temporary HACK: make sure that arith & bv are list-assoc
     // this may destroy some simplification steps such as max_bv_sharing
-    reduce_asserted_formulas(); 
+    reduce_asserted_formulas();
 
     CASSERT("well_sorted",check_well_sorted());
 
@@ -291,7 +291,7 @@ void asserted_formulas::reduce() {
 void asserted_formulas::eliminate_and() {
     IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";);
     set_eliminate_and(true);
-    reduce_asserted_formulas();    
+    reduce_asserted_formulas();
     TRACE("after_elim_and", display(tout););
 }
 
@@ -331,10 +331,10 @@ void asserted_formulas::display(std::ostream & out) const {
 void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
     if (!m_asserted_formulas.empty()) {
         unsigned sz = m_asserted_formulas.size();
-        for (unsigned i = 0; i < sz; i++) 
+        for (unsigned i = 0; i < sz; i++)
             ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false);
         out << "asserted formulas:\n";
-        for (unsigned i = 0; i < sz; i++) 
+        for (unsigned i = 0; i < sz; i++)
             out << "#" << m_asserted_formulas[i]->get_id() << " ";
         out << "\n";
     }
@@ -387,8 +387,12 @@ void asserted_formulas::find_macros_core() {
     expr_ref_vector  new_exprs(m);
     proof_ref_vector new_prs(m);
     unsigned sz = m_asserted_formulas.size();
-    m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, 
-                               m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
+    expr_dependency_ref_vector new_deps(m);
+    m_macro_finder->operator()(sz - m_asserted_qhead,
+                               m_asserted_formulas.c_ptr() + m_asserted_qhead,
+                               m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
+                               0, // 0 == No dependency tracking
+                               new_exprs, new_prs, new_deps);
     swap_asserted_formulas(new_exprs, new_prs);
     reduce_and_solve();
 }
@@ -409,12 +413,14 @@ void asserted_formulas::apply_quasi_macros() {
     IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
     TRACE("before_quasi_macros", display(tout););
     expr_ref_vector  new_exprs(m);
-    proof_ref_vector new_prs(m);      
-    quasi_macros proc(m, m_macro_manager, m_simplifier);    
-    while (proc(m_asserted_formulas.size() - m_asserted_qhead, 
-                m_asserted_formulas.c_ptr() + m_asserted_qhead, 
+    proof_ref_vector new_prs(m);
+    quasi_macros proc(m, m_macro_manager, m_simplifier);
+    expr_dependency_ref_vector new_deps(m);
+    while (proc(m_asserted_formulas.size() - m_asserted_qhead,
+                m_asserted_formulas.c_ptr() + m_asserted_qhead,
                 m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
-                new_exprs, new_prs)) {
+                0, // 0 == No dependency tracking
+                new_exprs, new_prs, new_deps)) {
         swap_asserted_formulas(new_exprs, new_prs);
         new_exprs.reset();
         new_prs.reset();
@@ -430,7 +436,7 @@ void asserted_formulas::nnf_cnf() {
     proof_ref_vector new_prs(m);
     expr_ref_vector  push_todo(m);
     proof_ref_vector push_todo_prs(m);
-    
+
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
@@ -460,8 +466,8 @@ void asserted_formulas::nnf_cnf() {
             CASSERT("well_sorted",is_well_sorted(m, r1));
             if (canceled()) {
                 return;
-            }        
-            
+            }
+
             if (m.proofs_enabled())
                 pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
             else
@@ -598,7 +604,7 @@ void asserted_formulas::propagate_values() {
     // C is a set which contains formulas of the form
     // { x = n }, where x is a variable and n a numeral.
     // R contains the rest.
-    // 
+    //
     // - new_exprs1 is the set C
     // - new_exprs2 is the set R
     //
@@ -663,7 +669,7 @@ void asserted_formulas::propagate_values() {
         // x->n will be removed from m_cache. If we don't do that, the next transformation
         // may simplify constraints in C using these entries, and the variables x in C
         // will be (silently) eliminated, and models produced by Z3 will not contain them.
-        flush_cache(); 
+        flush_cache();
     }
     TRACE("propagate_values", tout << "after:\n"; display(tout););
 }
@@ -786,7 +792,7 @@ void asserted_formulas::refine_inj_axiom() {
             TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);
             m_asserted_formulas.set(i, new_n);
             if (m.proofs_enabled()) {
-                proof_ref new_pr(m);     
+                proof_ref new_pr(m);
                 new_pr = m.mk_rewrite(n, new_n);
                 new_pr = m.mk_modus_ponens(pr, new_pr);
                 m_asserted_formula_prs.set(i, new_pr);
@@ -860,7 +866,7 @@ void asserted_formulas::max_bv_sharing() {
     }
     reduce_asserted_formulas();
     TRACE("bv_sharing", display(tout););
-    
+
 }
 
 #ifdef Z3DEBUG
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index 093680fd9..07f56f87e 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -49,7 +49,7 @@ class asserted_formulas {
 
     macro_manager               m_macro_manager;
     scoped_ptr<macro_finder>    m_macro_finder;
-    
+
     bit2int                     m_bit2int;
 
     maximise_bv_sharing         m_bv_sharing;
@@ -87,7 +87,7 @@ class asserted_formulas {
     bool apply_bit2int();
     void lift_ite();
     bool elim_bvs_from_quantifiers();
-    void ng_lift_ite(); 
+    void ng_lift_ite();
 #ifdef Z3DEBUG
     bool check_well_sorted() const;
 #endif
@@ -112,8 +112,8 @@ public:
     unsigned get_num_formulas() const { return m_asserted_formulas.size(); }
     unsigned get_formulas_last_level() const;
     unsigned get_qhead() const { return m_asserted_qhead; }
-    void commit(); 
-    void commit(unsigned new_qhead); 
+    void commit();
+    void commit(unsigned new_qhead);
     expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
     proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
     expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
@@ -129,7 +129,7 @@ public:
     void collect_statistics(statistics & st) const;
     // TODO: improve precision of the following method.
     bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ }
-    
+
     // -----------------------------------
     //
     // Macros
@@ -140,9 +140,7 @@ public:
     func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); }
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); }
     quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
-    // auxiliary function used to create a logic context based on a model.
-    void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
-
+    void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_macro_manager.insert(f, m, pr, dep); }
 };
 
 #endif /* ASSERTED_FORMULAS_H_ */
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index fecb42700..85633b7f4 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -209,7 +209,7 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
-                    m_ctx.add_rec_funs_to_model();            
+                    m_ctx.add_rec_funs_to_model();
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }
@@ -1568,7 +1568,7 @@ namespace smt {
         func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); }
         func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); }
         quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); }
-        void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); }
+        void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
     };
 
 };
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index e1e3b669b..bf8e08fb7 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -49,9 +49,9 @@ class macro_finder_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("macro-finder", *g);
-            fail_if_unsat_core_generation("macro-finder", g);
 
             bool produce_proofs = g->proofs_enabled();
+            bool unsat_core_enabled = g->unsat_core_enabled();
 
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
@@ -69,17 +69,21 @@ class macro_finder_tactic : public tactic {
 
             expr_ref_vector forms(m_manager), new_forms(m_manager);
             proof_ref_vector proofs(m_manager), new_proofs(m_manager);
-            unsigned   size = g->size();
+            expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
+            unsigned size = g->size();
             for (unsigned idx = 0; idx < size; idx++) {
                 forms.push_back(g->form(idx));
                 proofs.push_back(g->pr(idx));
+                deps.push_back(g->dep(idx));
             }
 
-            mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
+            mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
 
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
-                g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
+                g->assert_expr(new_forms.get(i),
+                               produce_proofs ? new_proofs.get(i) : 0,
+                               unsat_core_enabled ? new_deps.get(i) : 0);
 
             extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
             unsigned num = mm.get_num_macros();
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index ab68a2b63..c501559a5 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -35,22 +35,22 @@ class quasi_macros_tactic : public tactic {
         imp(ast_manager & m, params_ref const & p) : m_manager(m) {
             updt_params(p);
         }
-        
+
         ast_manager & m() const { return m_manager; }
-        
-        
-        void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
+
+
+        void operator()(goal_ref const & g,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("quasi-macros", *g);
-            fail_if_unsat_core_generation("quasi-macros", g);
 
             bool produce_proofs = g->proofs_enabled();
-            
+            bool produce_unsat_cores = g->unsat_core_enabled();
+
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
             bsimp->set_eliminate_and(true);
@@ -61,34 +61,40 @@ class quasi_macros_tactic : public tactic {
             bv_simplifier_params bv_params;
             bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
             simp.register_plugin(bvsimp);
-                
+
             macro_manager mm(m_manager, simp);
             quasi_macros qm(m_manager, mm, simp);
             bool more = true;
-        
+
             expr_ref_vector forms(m_manager), new_forms(m_manager);
             proof_ref_vector proofs(m_manager), new_proofs(m_manager);
+            expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
 
             unsigned size = g->size();
             for (unsigned i = 0; i < size; i++) {
                 forms.push_back(g->form(i));
                 proofs.push_back(g->pr(i));
+                deps.push_back(g->dep(i));
             }
-        
+
             while (more) { // CMW: use repeat(...) ?
                 if (m().canceled())
                     throw tactic_exception(m().limit().get_cancel_msg());
-            
+
                 new_forms.reset();
                 new_proofs.reset();
-                more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);            
+                new_deps.reset();
+                more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
                 forms.swap(new_forms);
-                proofs.swap(new_proofs);            
+                proofs.swap(new_proofs);
+                deps.swap(new_deps);
             }
 
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
-                g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
+                g->assert_expr(forms.get(i),
+                               produce_proofs ? proofs.get(i) : 0,
+                               produce_unsat_cores ? deps.get(i) : 0);
 
             extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
             unsigned num = mm.get_num_macros();
@@ -108,7 +114,7 @@ class quasi_macros_tactic : public tactic {
         void updt_params(params_ref const & p) {
         }
     };
-    
+
     imp *      m_imp;
     params_ref m_params;
 
@@ -121,7 +127,7 @@ public:
     virtual tactic * translate(ast_manager & m) {
         return alloc(quasi_macros_tactic, m, m_params);
     }
-        
+
     virtual ~quasi_macros_tactic() {
         dealloc(m_imp);
     }
@@ -136,19 +142,19 @@ public:
         insert_produce_models(r);
         insert_produce_proofs(r);
     }
-    
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-    
+
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
         imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }