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 01/16] 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 02/16] 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 03/16] 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 04/16] 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);
     }
 

From 3bfc3437f188394e246eed1668fdaef1e8ad8438 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Aug 2017 11:57:13 -0700
Subject: [PATCH 05/16] purify

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/arith_decl_plugin.cpp                 | 36 ++++-----------
 src/ast/arith_decl_plugin.h                   | 46 +++++--------------
 src/ast/rewriter/arith_rewriter.cpp           |  7 +--
 .../simplifier/arith_simplifier_plugin.cpp    |  2 -
 src/qe/nlqsat.cpp                             | 12 +----
 src/smt/theory_arith_core.h                   | 17 ++++---
 src/smt/theory_lra.cpp                        | 10 ++--
 src/tactic/arith/purify_arith_tactic.cpp      | 15 +++---
 8 files changed, 44 insertions(+), 101 deletions(-)

diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 01b671c99..03ee77458 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -215,18 +215,8 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_e = m->mk_const(e_decl);
     m->inc_ref(m_e);
 
-    func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
-    m_0_pw_0_int = m->mk_const(z_pw_z_int);
-    m->inc_ref(m_0_pw_0_int);
-
-    func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
-    m_0_pw_0_real = m->mk_const(z_pw_z_real);
-    m->inc_ref(m_0_pw_0_real);
 
     MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
-    MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
-    MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
-    MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
     MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r);
     MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r);
 }
@@ -279,12 +269,7 @@ arith_decl_plugin::arith_decl_plugin():
     m_atanh_decl(0),
     m_pi(0),
     m_e(0),
-    m_0_pw_0_int(0),
-    m_0_pw_0_real(0),
     m_neg_root_decl(0),
-    m_div_0_decl(0),
-    m_idiv_0_decl(0),
-    m_mod_0_decl(0),
     m_u_asin_decl(0),
     m_u_acos_decl(0),
     m_convert_int_numerals_to_real(false) {
@@ -339,12 +324,7 @@ void arith_decl_plugin::finalize() {
     DEC_REF(m_atanh_decl);
     DEC_REF(m_pi);
     DEC_REF(m_e);
-    DEC_REF(m_0_pw_0_int);
-    DEC_REF(m_0_pw_0_real);
     DEC_REF(m_neg_root_decl);
-    DEC_REF(m_div_0_decl);
-    DEC_REF(m_idiv_0_decl);
-    DEC_REF(m_mod_0_decl);
     DEC_REF(m_u_asin_decl);
     DEC_REF(m_u_acos_decl);
     m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr());
@@ -392,12 +372,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_ATANH:     return m_atanh_decl;
     case OP_PI:        return m_pi->get_decl();
     case OP_E:         return m_e->get_decl();
-    case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
-    case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
+    //case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
+    //case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
     case OP_NEG_ROOT:    return m_neg_root_decl;
-    case OP_DIV_0:       return m_div_0_decl;
-    case OP_IDIV_0:      return m_idiv_0_decl;
-    case OP_MOD_0:       return m_mod_0_decl;
+    //case OP_DIV_0:       return m_div_0_decl;
+    //case OP_IDIV_0:      return m_idiv_0_decl;
+    //case OP_MOD_0:       return m_mod_0_decl;
     case OP_U_ASIN:      return m_u_asin_decl;
     case OP_U_ACOS:      return m_u_acos_decl;
     default: return 0;
@@ -489,9 +469,9 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
 static bool is_const_op(decl_kind k) {
     return
         k == OP_PI ||
-        k == OP_E  ||
-        k == OP_0_PW_0_INT ||
-        k == OP_0_PW_0_REAL;
+        k == OP_E;
+        //k == OP_0_PW_0_INT ||
+        //k == OP_0_PW_0_REAL;
 }
 
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index a66ddd967..4b24ea5e6 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -70,12 +70,7 @@ enum arith_op_kind {
     OP_PI,
     OP_E,
     // under-specified symbols
-    OP_0_PW_0_INT,    // 0^0 for integers
-    OP_0_PW_0_REAL,   // 0^0 for reals
     OP_NEG_ROOT,      // x^n when n is even and x is negative
-    OP_DIV_0,         // x/0
-    OP_IDIV_0,        // x div 0
-    OP_MOD_0,         // x mod 0
     OP_U_ASIN,        // asin(x) for x < -1 or x > 1
     OP_U_ACOS,        // acos(x) for x < -1 or x > 1
     LAST_ARITH_OP
@@ -141,12 +136,7 @@ protected:
     app       * m_pi;
     app       * m_e;
 
-    app       * m_0_pw_0_int;
-    app       * m_0_pw_0_real;
     func_decl * m_neg_root_decl;
-    func_decl * m_div_0_decl;
-    func_decl * m_idiv_0_decl;
-    func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
     ptr_vector<app> m_small_ints;
@@ -207,10 +197,6 @@ public:
 
     app * mk_e() const { return m_e; }
 
-    app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
-
-    app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
-
     virtual expr * get_some_value(sort * s);
 
     virtual bool is_considered_uninterpreted(func_decl * f) {
@@ -218,12 +204,7 @@ public:
             return false;
         switch (f->get_decl_kind())
         {
-        case OP_0_PW_0_INT:
-        case OP_0_PW_0_REAL:
         case OP_NEG_ROOT:
-        case OP_DIV_0:
-        case OP_IDIV_0:
-        case OP_MOD_0:
         case OP_U_ASIN:
         case OP_U_ACOS:
             return true;
@@ -276,9 +257,9 @@ public:
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
     bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
     bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
-    bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
+    //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
     bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
-    bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
+    //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
     bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
     bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
     bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
@@ -389,16 +370,16 @@ public:
     app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
     app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); }
 
-    app * mk_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
-    app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
-    app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
+    app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
+    app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
+    app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
 
-    app * mk_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
-    app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
-    app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
-    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
-    app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
-    app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
+    app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
+    app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
+    app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
+    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
+    app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
+    app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
     app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); }
     app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }
     app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); }
@@ -425,11 +406,6 @@ public:
     app * mk_pi() { return plugin().mk_pi(); }
     app * mk_e()  { return plugin().mk_e(); }
 
-    app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
-    app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
-    app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
-    app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
-    app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
     app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
     app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
     app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 18556b71b..fc9b1ac1d 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -680,8 +680,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     if (m_util.is_numeral(arg2, v2, is_int)) {
         SASSERT(!is_int);
         if (v2.is_zero()) {
-            result = m_util.mk_div0(arg1);
-            return BR_REWRITE1;
+            return BR_FAILED;
         }
         else if (m_util.is_numeral(arg1, v1, is_int)) {
             result = m_util.mk_numeral(v1/v2, false);
@@ -734,10 +733,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
-        result = m_util.mk_idiv0(arg1);
-        return BR_REWRITE1;
-    }
     return BR_FAILED;
 }
 
diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp
index 8410ce143..bfe72b232 100644
--- a/src/ast/simplifier/arith_simplifier_plugin.cpp
+++ b/src/ast/simplifier/arith_simplifier_plugin.cpp
@@ -405,8 +405,6 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     case OP_POWER:                    return false;
     case OP_ABS:      SASSERT(num_args == 1); mk_abs(args[0], result); break;
     case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
-    case OP_DIV_0: return false;
-    case OP_IDIV_0: return false;
     default:
         return false;
     }
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 0f2437982..3e5a9f24f 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -444,16 +444,12 @@ namespace qe {
             div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {}
             ~div_rewriter_cfg() {}
             br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
-                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) {                    
+                rational r;
+                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && (!a.is_numeral(args[1], r) || r.is_zero())) {                    
                     result = m.mk_fresh_const("div", a.mk_real());
                     m_divs.push_back(div(m, args[0], args[1], to_app(result)));
                     return BR_DONE;
                 }
-                if (is_decl_of(f, a.get_family_id(), OP_DIV_0) && sz == 1 && !a.is_numeral(args[0])) {                    
-                    result = m.mk_fresh_const("div", a.mk_real());
-                    m_divs.push_back(div(m, args[0], m_zero, to_app(result)));
-                    return BR_DONE;
-                }
                 return BR_FAILED;
             }
             vector<div> const& divs() const { return m_divs; }
@@ -507,10 +503,6 @@ namespace qe {
                     m_has_divs = true;
                     return;
                 }
-                if (a.is_div0(n) && s.m_mode == qsat_t) {
-                    m_has_divs = true;
-                    return;
-                }
                 TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";);
                 throw tactic_exception("not NRA");
             }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index a30e51133..b5e7db310 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -395,7 +395,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
@@ -406,7 +407,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_idiv(app * n) {
-        found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         app * mod         = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
@@ -419,7 +421,8 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -429,7 +432,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
         if (!ctx.relevancy()) {
@@ -734,11 +738,6 @@ namespace smt {
             return internalize_div(n);
         else if (m_util.is_idiv(n))
             return internalize_idiv(n);
-        else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) {
-            ctx.internalize(n->get_arg(0), false);
-            enode * e = mk_enode(n);
-            return mk_var(e);
-        }
         else if (m_util.is_mod(n)) 
             return internalize_mod(n);
         else if (m_util.is_rem(n)) 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 124fea910..c5e3ae350 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -292,9 +292,6 @@ namespace smt {
         }
 
         void found_not_handled(expr* n) {
-            if (a.is_div0(n)) {
-                return;
-            }
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
                 m_underspecified.push_back(to_app(n));
@@ -379,7 +376,12 @@ namespace smt {
                 }
                 else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
                     app* t = to_app(n);
-                    found_not_handled(n);
+                    if (a.is_div(n, n1, n2) && is_numeral(n2, r)) {
+                        // skip
+                    }
+                    else {
+                        found_not_handled(n);
+                    }
                     internalize_args(t);
                     mk_enode(t);
                     theory_var v = mk_var(n);
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 0443a51ed..7e89794ce 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -297,11 +297,11 @@ struct purify_arith_proc {
             push_cnstr(OR(EQ(y, mk_real_zero()),
                           EQ(u().mk_mul(y, k), x)));
             push_cnstr_pr(result_pr);
-
-            if (complete()) {
+            rational r;
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
                 // y != 0 \/ k = div-0(x)
                 push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
-                              EQ(k, u().mk_div0(x))));
+                              EQ(k, u().mk_div(x, mk_real_zero()))));
                 push_cnstr_pr(result_pr);
             }
         }
@@ -348,11 +348,12 @@ struct purify_arith_proc {
             push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y))));
             push_cnstr_pr(mod_pr);
 
-            if (complete()) {
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x))));
+            rational r;
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero))));
                 push_cnstr_pr(result_pr);
 
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x))));
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero))));
                 push_cnstr_pr(mod_pr);
             }
         }
@@ -414,7 +415,7 @@ struct purify_arith_proc {
                 // (^ x 0) --> k  |  x != 0 implies k = 1,   x = 0 implies k = 0^0 
                 push_cnstr(OR(EQ(x, zero), EQ(k, one)));
                 push_cnstr_pr(result_pr);
-                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
+                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, u().mk_power(zero, zero))));
                 push_cnstr_pr(result_pr);
             }
             else if (!is_int) {

From ce8443581d31b4194f6db010d91f9dab8ee55aac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Aug 2017 12:15:27 -0700
Subject: [PATCH 06/16] add API methods for creating and modifying models,
 #1223

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp | 63 +++++++++++++++++++++++++++++++++++++++++++
 src/api/c++/z3++.h    | 20 ++++++++++++++
 src/api/z3_api.h      | 54 +++++++++++++++++++++++++++++++++++++
 3 files changed, 137 insertions(+)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index de917650d..66002baa0 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -30,6 +30,17 @@ Revision History:
 
 extern "C" {
 
+    Z3_model Z3_API Z3_mk_model(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_mk_model(c);
+        RESET_ERROR_CODE();
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
+        m_ref->m_model = alloc(model, mk_c(c)->m());
+        mk_c(c)->save_object(m_ref);
+        RETURN_Z3(of_model(m_ref));
+        Z3_CATCH_RETURN(0);
+    }
+
     void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m) {
         Z3_TRY;
         LOG_Z3_model_inc_ref(c, m);
@@ -224,6 +235,31 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) {
+        Z3_TRY;
+        LOG_Z3_add_func_interp(c, m, f, else_val);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); 
+        f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity());
+        mk_c(c)->save_object(f_ref);
+        mdl->register_decl(d, f_ref->m_func_interp);
+        f_ref->m_func_interp->set_else(to_expr(else_val));
+        RETURN_Z3(of_func_interp(f_ref));
+        Z3_CATCH_RETURN(0);        
+    }
+
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_add_const_interp(c, m, f, a);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        mdl->register_decl(d, to_expr(a));
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f) {
         Z3_TRY;
         LOG_Z3_func_interp_inc_ref(c, f);
@@ -283,6 +319,15 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value) {
+        Z3_TRY;
+        LOG_Z3_func_interp_set_else(c, f, else_value);
+        RESET_ERROR_CODE();
+        // CHECK_NON_NULL(f, 0);
+        to_func_interp_ref(f)->set_else(to_expr(else_value));
+        Z3_CATCH;
+    }
+
     unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f) {
         Z3_TRY;
         LOG_Z3_func_interp_get_arity(c, f);
@@ -292,6 +337,24 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) {
+        Z3_TRY;
+        LOG_Z3_add_func_entry(c, fi, args, value);
+        //CHECK_NON_NULL(fi, void);
+        //CHECK_NON_NULL(args, void);
+        //CHECK_NON_NULL(value, void);
+        func_interp* _fi = to_func_interp_ref(fi);
+        expr* _value = to_expr(value);
+        if (to_ast_vector_ref(args).size() != _fi->get_arity()) {
+            SET_ERROR_CODE(Z3_IOB);
+            return;
+        }
+        // check sorts of value
+        expr* const* _args = (expr* const*) to_ast_vector_ref(args).c_ptr();
+        _fi->insert_entry(_args, _value);
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e) {
         Z3_TRY;
         LOG_Z3_func_entry_inc_ref(c, e);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 42db6f352..2f67cb72a 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1731,6 +1731,14 @@ namespace z3 {
         expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
         unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
         func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
+        void add_entry(expr_vector const& args, expr& value) {
+            Z3_add_func_entry(ctx(), m_interp, args, value);
+            check_error();
+        }
+        void set_else(expr& value) {
+            Z3_func_entry_set_else(ctx(), m_interp, value);
+            check_error();
+        }
     };
 
     class model : public object {
@@ -1740,6 +1748,7 @@ namespace z3 {
             Z3_model_inc_ref(ctx(), m);
         }
     public:
+        model(context & c):object(c) { init(Z3_mk_model(c)); }
         model(context & c, Z3_model m):object(c) { init(m); }
         model(model const & s):object(s) { init(s.m_model); }
         ~model() { Z3_model_dec_ref(ctx(), m_model); }
@@ -1795,6 +1804,17 @@ namespace z3 {
             return 0 != Z3_model_has_interp(ctx(), m_model, f);
         }
 
+        func_interp add_func_interp(func_decl& f, expr& else_val) {
+            Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
+            check_error();
+            return func_interp(ctx(), r);
+        }
+
+        void add_const_interp(func_decl& f, expr& value) {
+            Z3_add_const_interp(ctx(), m_model, f, value);
+            check_error();
+        }
+
         friend std::ostream & operator<<(std::ostream & out, model const & m);
     };
     inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 43c175ca8..045417d38 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4680,6 +4680,14 @@ extern "C" {
 
     /** @name Models */
     /*@{*/
+
+    /**
+       \brief Create a fresh model object. It has reference count 0.
+
+       def_API('Z3_mk_model', MODEL, (_in(CONTEXT),))
+    */
+    Z3_model Z3_API Z3_mk_model(Z3_context c);
+
     /**
        \brief Increment the reference counter of the given model.
 
@@ -4850,6 +4858,26 @@ extern "C" {
     */
     Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
 
+    /**
+       \brief Create a fresh func_interp object, add it to a model for a specified function. 
+       It has reference count 0.       
+
+       \param c context
+       \param m model
+       \param f function declaration 
+       \param default_value default value for function interpretation
+
+       def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+    */
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
+
+    /**
+       \brief Add a constant interpretation.
+
+       def_API('Z3_add_const_interp', VOID, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+     */
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
+
     /**
        \brief Increment the reference counter of the given Z3_func_interp object.
 
@@ -4897,6 +4925,16 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
 
+    /**
+       \brief Return the 'else' value of the given function interpretation.
+
+       A function interpretation is represented as a finite map and an 'else' value.
+       This procedure can be used to update the 'else' value.
+
+       def_API('Z3_func_interp_set_else', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST)))
+    */
+    void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
+
     /**
        \brief Return the arity (number of arguments) of the given function interpretation.
 
@@ -4904,6 +4942,22 @@ extern "C" {
     */
     unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
 
+    /**
+       \brief add a function entry to a function interpretation.
+
+       \param c logical context
+       \param fi a function interpregation to be updated.
+       \param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
+       \param value value of the function when the parameters match args.
+
+       It is assumed that entries added to a function cover disjoint arguments. 
+       If an two entries are added with the same arguments, only the second insertion survives and the
+       first inserted entry is removed.
+
+       def_API('Z3_add_func_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))
+     */
+    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
+
     /**
        \brief Increment the reference counter of the given Z3_func_entry object.
 

From 623cd5ded2bbc414faca3ca2295d62c935c026f0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Aug 2017 13:00:43 -0700
Subject: [PATCH 07/16] fix naming for functions #1223

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp | 4 ++--
 src/api/c++/z3++.h    | 4 ++--
 src/api/z3_api.h      | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 66002baa0..540f014c6 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -337,9 +337,9 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) {
+    void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) {
         Z3_TRY;
-        LOG_Z3_add_func_entry(c, fi, args, value);
+        LOG_Z3_func_interp_add_entry(c, fi, args, value);
         //CHECK_NON_NULL(fi, void);
         //CHECK_NON_NULL(args, void);
         //CHECK_NON_NULL(value, void);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 2f67cb72a..6d8ff3b35 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1732,11 +1732,11 @@ namespace z3 {
         unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
         func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
         void add_entry(expr_vector const& args, expr& value) {
-            Z3_add_func_entry(ctx(), m_interp, args, value);
+            Z3_func_interp_add_entry(ctx(), m_interp, args, value);
             check_error();
         }
         void set_else(expr& value) {
-            Z3_func_entry_set_else(ctx(), m_interp, value);
+            Z3_func_interp_set_else(ctx(), m_interp, value);
             check_error();
         }
     };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 045417d38..bed70cb6c 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4954,9 +4954,9 @@ extern "C" {
        If an two entries are added with the same arguments, only the second insertion survives and the
        first inserted entry is removed.
 
-       def_API('Z3_add_func_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))
+       def_API('Z3_func_interp_add_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))
      */
-    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
+    void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
 
     /**
        \brief Increment the reference counter of the given Z3_func_entry object.

From 5db349f6fafc5b117dd49e11d7f2cd42531732af Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Aug 2017 23:52:27 -0700
Subject: [PATCH 08/16] raise an exception if trying proof generation for the
 SAT solver. Stackoverflow question 
 https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver/inc_sat_solver.cpp         | 3 +++
 src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 521aa5e71..21f9f1e8a 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -388,6 +388,9 @@ private:
         m_subgoals.reset();
         init_preprocess();
         SASSERT(g->models_enabled());
+        if (g->proofs_enabled()) {
+            throw default_exception("generation of proof objects is not supported in this mode");
+        }
         SASSERT(!g->proofs_enabled());
         TRACE("sat", g->display(tout););
         try {
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 0ad9e5f19..3e77b7abc 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_qffpbv_tactic(m, p);
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
-    else if (logic == "QF_FD" || logic == "SAT")
+    else if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
         return mk_solver2tactic(mk_fd_solver(m, p));
     //else if (logic=="QF_UFNRA")
     //    return mk_qfufnra_tactic(m, p);
@@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
 }
 
 static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
-    if (logic == "QF_FD" || logic == "SAT") 
+    if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
         return mk_fd_solver(m, p);
     return 0;
 }

From 8542e4ae3df20070e9922b5e25e7381b6985ceb7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Aug 2017 00:05:53 -0700
Subject: [PATCH 09/16] add pre-processing simplificaiton of power to the
 legacy simplifier Fixes #1237

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../simplifier/arith_simplifier_plugin.cpp    | 21 ++++++++++++++++++-
 src/ast/simplifier/arith_simplifier_plugin.h  |  1 +
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp
index bfe72b232..d604ba2ff 100644
--- a/src/ast/simplifier/arith_simplifier_plugin.cpp
+++ b/src/ast/simplifier/arith_simplifier_plugin.cpp
@@ -402,7 +402,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     case OP_TO_REAL:  SASSERT(num_args == 1); mk_to_real(args[0], result); break;
     case OP_TO_INT:   SASSERT(num_args == 1); mk_to_int(args[0], result); break;
     case OP_IS_INT:   SASSERT(num_args == 1); mk_is_int(args[0], result); break;
-    case OP_POWER:                    return false;
+    case OP_POWER:    SASSERT(num_args == 2); mk_power(args[0], args[1], result); break;
     case OP_ABS:      SASSERT(num_args == 1); mk_abs(args[0], result); break;
     case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
     default:
@@ -412,6 +412,25 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     return true;
 }
 
+void arith_simplifier_plugin::mk_power(expr* x, expr* y, expr_ref& result) {
+    rational a, b;
+    if (is_numeral(y, b) && b.is_one()) {
+        result = x;
+        return;
+    }
+    if (is_numeral(x, a) && is_numeral(y, b) && b.is_unsigned()) {
+        if (b.is_zero() && !a.is_zero()) {
+            result = m_util.mk_numeral(rational(1), m_manager.get_sort(x));
+            return;
+        }
+        if (!b.is_zero()) {
+            result = m_util.mk_numeral(power(a, b.get_unsigned()), m_manager.get_sort(x));
+            return;
+        }
+    }
+    result = m_util.mk_power(x, y);
+}
+
 void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) {
     expr_ref c(m_manager);
     expr_ref m_arg(m_manager);
diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h
index 21ab8f6b4..4f3a6add0 100644
--- a/src/ast/simplifier/arith_simplifier_plugin.h
+++ b/src/ast/simplifier/arith_simplifier_plugin.h
@@ -82,6 +82,7 @@ public:
     void mk_to_real(expr * arg, expr_ref & result);
     void mk_to_int(expr * arg, expr_ref & result);
     void mk_is_int(expr * arg, expr_ref & result);
+    void mk_power(expr* x, expr* y, expr_ref& result);
     void mk_abs(expr * arg, expr_ref & result);
 
     virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);

From 974eaab01c752df9d61d53887709a5eb9a71ef1d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Aug 2017 01:38:23 -0700
Subject: [PATCH 10/16] complement regular expressions when used in negated
 membership constraints #1224

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                           |  1 +
 src/math/automata/automaton.h             | 59 +++++++++++------------
 src/math/automata/symbolic_automata.h     |  3 +-
 src/math/automata/symbolic_automata_def.h | 17 +++++--
 src/smt/theory_seq.cpp                    | 20 +++++---
 5 files changed, 58 insertions(+), 42 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f347a8e49..4f9a88490 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1726,6 +1726,7 @@ ast * ast_manager::register_node_core(ast * n) {
     }
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
+    static unsigned s_counter = 0;
 
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index cf4dcbfc6..2f55d5cc2 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -107,11 +107,10 @@ public:
         m_init = init;
         m_delta.push_back(moves());
         m_delta_inv.push_back(moves());
-        for (unsigned i = 0; i < final.size(); ++i) {
-            add_to_final_states(final[i]);
+        for (unsigned f : final) {
+            add_to_final_states(f);
         }
-        for (unsigned i = 0; i < mvs.size(); ++i) {
-            move const& mv = mvs[i];
+        for (move const& mv : mvs) {
             unsigned n = std::max(mv.src(), mv.dst());
             if (n >= m_delta.size()) {
                 m_delta.resize(n+1, moves());
@@ -280,8 +279,8 @@ public:
         }
         else {
             init = a.num_states();
-            for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
-                mvs.push_back(move(m, init, a.m_final_states[i]));
+            for (unsigned st : a.m_final_states) {
+                mvs.push_back(move(m, init, st));
             }
         }
         return alloc(automaton, m, init, final, mvs);        
@@ -471,18 +470,17 @@ public:
     moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
     bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
     bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
-	bool is_final_configuration(uint_set s) const { 
-		for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
-			if (is_final_state(*it))
-				return true;
-		}
-		return false; 
-	}
+    bool is_final_configuration(uint_set s) const {
+        for (unsigned i : s) {
+            if (is_final_state(i))
+                return true;
+        }
+        return false; 
+    }
     bool is_epsilon_free() const {
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            moves const& mvs = m_delta[i];
-            for (unsigned j = 0; j < mvs.size(); ++j) {
-                if (!mvs[j].t()) return false;
+        for (moves const& mvs : m_delta) {
+            for (move const & m : mvs) {
+                if (!m.t()) return false;
             }
         }
         return true;
@@ -490,8 +488,8 @@ public:
 
     bool all_epsilon_in(unsigned s) {
         moves const& mvs = m_delta_inv[s];
-        for (unsigned j = 0; j < mvs.size(); ++j) {
-            if (mvs[j].t()) return false;
+        for (move const& m : mvs) {
+            if (m.t()) return false;
         }
         return true;
     }
@@ -504,15 +502,15 @@ public:
     bool is_loop_state(unsigned s) const {
         moves mvs;
         get_moves_from(s, mvs);
-        for (unsigned i = 0; i < mvs.size(); ++i) {
-            if (s == mvs[i].dst()) return true;
+        for (move const& m : mvs) {
+            if (s == m.dst()) return true;
         }
         return false;
     }
 
     unsigned move_count() const {
         unsigned result = 0;
-        for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {}
+        for (moves const& mvs : m_delta) result += mvs.size();
         return result;
     }
     void get_epsilon_closure(unsigned state, unsigned_vector& states) {
@@ -524,13 +522,13 @@ public:
     void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
         get_moves(state, m_delta, mvs, epsilon_closure);
     }
-	void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
-		for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) {
-			moves curr;
-			get_moves(*it, m_delta, curr, epsilon_closure);
-			mvs.append(curr);
-		}
-	}
+    void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
+        for (unsigned i : states) {
+            moves curr;
+            get_moves(i, m_delta, curr, epsilon_closure);
+            mvs.append(curr);
+        }
+    }
     void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
         get_moves(state, m_delta_inv, mvs, epsilon_closure);
     }
@@ -543,8 +541,7 @@ public:
         out << "\n";
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             moves const& mvs = m_delta[i];
-            for (unsigned j = 0; j < mvs.size(); ++j) {
-                move const& mv = mvs[j];
+            for (move const& mv : mvs) {
                 out << i << " -> " << mv.dst() << " ";
                 if (mv.t()) {
                     out << "if "; 
diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index 4a8e7a74d..35545e975 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -136,7 +136,8 @@ private:
             
             //false case
             curr_bv.push_back(false);
-            ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m);
+			ref_t neg(m_ba.mk_not(constraints[i]), m);
+            ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
             curr_bv.pop_back();
         }
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index c1ee53214..aa8dd34fd 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -288,7 +288,7 @@ typename symbolic_automata<T, M>::automaton_t*
 symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance) {
     vector<std::pair<vector<bool>, ref_t> > min_terms;
     vector<ref_t> predicates;
-    
+
     map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id; // set of states to unique id
     vector<uint_set> id2s;                           // unique id to set of b-states
     uint_set set;
@@ -296,9 +296,19 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
     moves_t new_mvs;                                 // moves in the resulting automaton
     unsigned_vector new_final_states;                // new final states
     unsigned p_state_id = 0;                         // next state identifier
-    
+
+    TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
     // adds non-final states of a to final if flipping and and final otherwise
-    if (a.is_final_configuration(set) != flip_acceptance) {
+    unsigned_vector init_states;
+    a.get_epsilon_closure(a.init(), init_states);
+    bool found_final = false;
+    for (unsigned s : init_states) {
+        if (a.is_final_state(s)) {
+            found_final = true;
+            break;
+        }
+    }
+    if (found_final != flip_acceptance) {
         new_final_states.push_back(p_state_id);
     }
     
@@ -342,6 +352,7 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
             
             bool is_new = !s2id.contains(set);
             if (is_new) {
+                TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
                 if (a.is_final_configuration(set) != flip_acceptance) {
                     new_final_states.push_back(p_state_id);
                 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c91882dad..a32a4833a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3391,15 +3391,22 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
         return;
     }
 
-    eautomaton* a = get_automaton(e2);
+    expr_ref e3(e2, m);
+    context& ctx = get_context();
+    literal lit = ctx.get_literal(n);
+    if (!is_true) {
+        e3 = m_util.re.mk_complement(e2);
+        is_true = true;
+        lit.neg();
+    }
+    eautomaton* a = get_automaton(e3);
     if (!a) return;
 
-    context& ctx = get_context();
 
     expr_ref len(m_util.str.mk_length(e1), m);
     for (unsigned i = 0; i < a->num_states(); ++i) {
-        literal acc = mk_accept(e1, len, e2, i);
-        literal rej = mk_reject(e1, len, e2, i);
+        literal acc = mk_accept(e1, len, e3, i);
+        literal rej = mk_reject(e1, len, e3, i);
         add_axiom(a->is_final_state(i)?acc:~acc);
         add_axiom(a->is_final_state(i)?~rej:rej);
     }
@@ -3408,17 +3415,16 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     unsigned_vector states;
     a->get_epsilon_closure(a->init(), states);
     literal_vector lits;
-    literal lit = ctx.get_literal(n);
     if (is_true) {
         lits.push_back(~lit);
     }
     for (unsigned i = 0; i < states.size(); ++i) {
         if (is_true) {
-            lits.push_back(mk_accept(e1, zero, e2, states[i]));
+            lits.push_back(mk_accept(e1, zero, e3, states[i]));
         }
         else {
             literal nlit = ~lit;
-            propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e2, states[i]));
+            propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i]));
         }
     }
     if (is_true) {

From 0ebb9172681e11b6ac0bcea6a4d69b021282a21a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Aug 2017 01:40:15 -0700
Subject: [PATCH 11/16] complement regular expressions when used in negated
 membership constraints #1224

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                       | 2 --
 src/math/automata/symbolic_automata.h | 4 ++--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 4f9a88490..5c0abf6b8 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1726,8 +1726,6 @@ ast * ast_manager::register_node_core(ast * n) {
     }
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
-    static unsigned s_counter = 0;
-
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index 35545e975..4831280af 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -130,13 +130,13 @@ private:
         else {
             //true case
             curr_bv.push_back(true);
-            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);			
+            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
             curr_bv.pop_back();
             
             //false case
             curr_bv.push_back(false);
-			ref_t neg(m_ba.mk_not(constraints[i]), m);
+            ref_t neg(m_ba.mk_not(constraints[i]), m);
             ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
             curr_bv.pop_back();

From feac705cb88bb00085e8c4313dbdc23befc7aa0c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Aug 2017 13:47:19 -0700
Subject: [PATCH 12/16] include epsilon closure in initial state set,
 streamline final configuration computation #1224

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/automata/symbolic_automata_def.h | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index aa8dd34fd..c89080d3d 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -298,21 +298,16 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
     unsigned p_state_id = 0;                         // next state identifier
 
     TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
-    // adds non-final states of a to final if flipping and and final otherwise
+    // adds non-final states of a to final if flipping and final otherwise
     unsigned_vector init_states;
-    a.get_epsilon_closure(a.init(), init_states);
-    bool found_final = false;
+    a.get_epsilon_closure(a.init(), init_states);    
     for (unsigned s : init_states) {
-        if (a.is_final_state(s)) {
-            found_final = true;
-            break;
-        }
+        set.insert(s);
     }
-    if (found_final != flip_acceptance) {
+    if (a.is_final_configuration(set) != flip_acceptance) {
         new_final_states.push_back(p_state_id);
     }
     
-    set.insert(a.init());                         // Initial state as aset
     s2id.insert(set, p_state_id++);               // the index to the initial state is 0
     id2s.push_back(set);
     

From 1a1c705376677376cc9f8e63896e136f91b6c7eb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 30 Aug 2017 19:34:31 +0100
Subject: [PATCH 13/16] Added global model completion for the SMT2 frontend.

---
 src/cmd_context/cmd_context.cpp | 97 +++++++++++++++++++++++++++++----
 src/cmd_context/cmd_context.h   | 47 ++++++++--------
 src/cmd_context/pdecl.cpp       | 79 ++++++++++++++-------------
 src/cmd_context/pdecl.h         | 13 +++--
 src/model/model_params.pyg      |  3 +-
 5 files changed, 164 insertions(+), 75 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f172e5e93..acbdc0bcf 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -229,6 +229,28 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const *
     return find(num_args, sorts.c_ptr(), range);
 }
 
+unsigned func_decls::get_num_entries() const {
+    if (!more_than_one())
+        return 1;
+
+    func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+    return fs->size();
+}
+
+func_decl * func_decls::get_entry(unsigned inx) {
+    if (!more_than_one()) {
+        SASSERT(inx == 0);
+        return first();
+    }
+    else {
+        func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+        auto b = fs->begin();
+        for (unsigned i = 0; i < inx; i++)
+            b++;
+        return *b;
+    }
+}
+
 void macro_decls::finalize(ast_manager& m) {
     for (auto v : *m_decls) m.dec_ref(v.m_body);
     dealloc(m_decls);
@@ -288,13 +310,13 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
     }
     else {
         VERIFY(decls.insert(m(), arity, domain, t));
-    }    
+    }
 }
 
 void cmd_context::erase_macro(symbol const& s) {
     macro_decls decls;
     VERIFY(m_macros.find(s, decls));
-    decls.erase_last(m());    
+    decls.erase_last(m());
 }
 
 bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const {
@@ -870,11 +892,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     }
 
     //
-    // disable warning given the current way they are used 
-    // (Z3 will here silently assume and not check the definitions to be well founded, 
+    // disable warning given the current way they are used
+    // (Z3 will here silently assume and not check the definitions to be well founded,
     // and please use HSF for everything else).
     //
-    if (false && !ids.empty() && !m_rec_fun_declared) {        
+    if (false && !ids.empty() && !m_rec_fun_declared) {
         warning_msg("recursive function definitions are assumed well-founded");
         m_rec_fun_declared = true;
     }
@@ -953,7 +975,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
         return f;
     }
 
-    if (contains_macro(s, arity, domain)) 
+    if (contains_macro(s, arity, domain))
         throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
 
     if (num_indices > 0)
@@ -1316,7 +1338,7 @@ void cmd_context::push(unsigned n) {
         push();
 }
 
-void cmd_context::restore_func_decls(unsigned old_sz) {    
+void cmd_context::restore_func_decls(unsigned old_sz) {
     SASSERT(old_sz <= m_func_decls_stack.size());
     svector<sf_pair>::iterator it  = m_func_decls_stack.begin() + old_sz;
     svector<sf_pair>::iterator end = m_func_decls_stack.end();
@@ -1418,7 +1440,7 @@ void cmd_context::pop(unsigned n) {
     restore_assertions(s.m_assertions_lim);
     restore_psort_inst(s.m_psort_inst_stack_lim);
     m_scopes.shrink(new_lvl);
-    
+
 }
 
 void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
@@ -1488,6 +1510,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     if (r == l_true) {
+        complete_model();
         validate_model();
     }
     validate_check_sat_result(r);
@@ -1548,7 +1571,7 @@ void cmd_context::reset_assertions() {
         if (m_solver) m_solver->push();
     }
 }
-    
+
 
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
@@ -1632,6 +1655,60 @@ struct contains_array_op_proc {
     void operator()(quantifier * n) {}
 };
 
+/**
+    \brief Complete the model if necessary.
+*/
+void cmd_context::complete_model() {
+    if (!is_model_available() ||
+        gparams::get_value("model.completion") != "true")
+        return;
+
+    model_ref md;
+    get_check_sat_result()->get_model(md);
+    SASSERT(md.get() != 0);
+    params_ref p;
+    p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
+    p.set_uint("sort_store", true);
+    p.set_bool("completion", true);
+    model_evaluator evaluator(*(md.get()), p);
+    evaluator.set_expand_array_equalities(false);
+
+    scoped_rlimit _rlimit(m().limit(), 0);
+    cancel_eh<reslimit> eh(m().limit());
+    expr_ref r(m());
+    scoped_ctrl_c ctrlc(eh);
+
+    for (auto kd : m_psort_decls) {
+        symbol const & k = kd.m_key;
+        psort_decl * v = kd.m_value;
+        if (v->is_user_decl()) {
+            SASSERT(!v->has_var_params());
+            IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+            ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
+            sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.c_ptr());
+            if (!md->has_uninterpreted_sort(srt)) {
+                expr * singleton = m().get_some_value(srt);
+                md->register_usort(srt, 1, &singleton);
+            }
+        }
+    }
+
+    for (auto kd : m_func_decls) {
+        symbol const & k = kd.m_key;
+        func_decls & v = kd.m_value;
+        IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+        for (unsigned i = 0; i < v.get_num_entries(); i++) {
+            func_decl * f = v.get_entry(i);
+            if (!md->has_interpretation(f)) {
+                sort * range = f->get_range();
+                func_interp * fi = alloc(func_interp, m(), f->get_arity());
+                fi->set_else(m().get_some_value(range));
+                md->register_decl(f, fi);
+            }
+        }
+    }
+}
+
 /**
    \brief Check if the current model satisfies the quantifier free formulas.
 */
@@ -1918,7 +1995,7 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
     }
     if (m_owner.m_scopes.size() > 0) {
         m_owner.m_psort_inst_stack.push_back(pd);
-        
+
     }
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 189863e58..5883a8d8e 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -8,7 +8,7 @@ Module Name:
 Abstract:
     Ultra-light command context.
     It provides a generic command pluging infrastructure.
-    A command context also provides names (aka symbols) to Z3 objects. 
+    A command context also provides names (aka symbols) to Z3 objects.
     These names are used to reference Z3 objects in commands.
 
 Author:
@@ -58,6 +58,8 @@ public:
     func_decl * first() const;
     func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
     func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
+    unsigned get_num_entries() const;
+    func_decl * get_entry(unsigned inx);
 };
 
 struct macro_decl {
@@ -66,18 +68,18 @@ struct macro_decl {
 
     macro_decl(unsigned arity, sort *const* domain, expr* body):
         m_domain(arity, domain), m_body(body) {}
-    
+
     void dec_ref(ast_manager& m) { m.dec_ref(m_body); }
-    
+
 };
 
 class macro_decls {
     vector<macro_decl>* m_decls;
-public:    
+public:
     macro_decls() { m_decls = 0; }
     void finalize(ast_manager& m);
     bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
-    expr* find(unsigned arity, sort *const* domain) const;    
+    expr* find(unsigned arity, sort *const* domain) const;
     void erase_last(ast_manager& m);
     vector<macro_decl>::iterator begin() const { return m_decls->begin(); }
     vector<macro_decl>::iterator end() const { return m_decls->end(); }
@@ -158,11 +160,11 @@ public:
     enum status {
         UNSAT, SAT, UNKNOWN
     };
-    
+
     enum check_sat_state {
         css_unsat, css_sat, css_unknown, css_clear
     };
-    
+
     typedef std::pair<unsigned, expr*> macro;
 
     struct scoped_watch {
@@ -188,7 +190,7 @@ protected:
     bool                         m_ignore_check;      // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
     bool                         m_processing_pareto; // used when re-entering check-sat for pareto front.
     bool                         m_exit_on_error;
-    
+
     static std::ostringstream    g_error_stream;
 
     ast_manager *                m_manager;
@@ -200,7 +202,7 @@ protected:
     check_logic                  m_check_logic;
     stream_ref                   m_regular;
     stream_ref                   m_diagnostic;
-    dictionary<cmd*>             m_cmds;    
+    dictionary<cmd*>             m_cmds;
     dictionary<builtin_decl>     m_builtin_decls;
     scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
@@ -217,7 +219,7 @@ protected:
     svector<symbol>              m_macros_stack;
     ptr_vector<pdecl>            m_psort_inst_stack;
 
-    // 
+    //
     ptr_vector<pdecl>            m_aux_pdecls;
     ptr_vector<expr>             m_assertions;
     std::vector<std::string>     m_assertion_strings;
@@ -236,7 +238,7 @@ protected:
     svector<scope>               m_scopes;
     scoped_ptr<solver_factory>   m_solver_factory;
     scoped_ptr<solver_factory>   m_interpolating_solver_factory;
-    ref<solver>                  m_solver;    
+    ref<solver>                  m_solver;
     ref<check_sat_result>        m_check_sat_result;
     ref<opt_wrapper>             m_opt;
 
@@ -296,7 +298,7 @@ protected:
 
     bool contains_macro(symbol const& s) const;
     bool contains_macro(symbol const& s, func_decl* f) const;
-    bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const;    
+    bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const;
     void insert_macro(symbol const& s, unsigned arity, sort*const* domain, expr* t);
     void erase_macro(symbol const& s);
     bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
@@ -304,7 +306,7 @@ protected:
 
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
-    ~cmd_context(); 
+    ~cmd_context();
     void set_cancel(bool f);
     context_params  & params() { return m_params; }
     solver_factory &get_solver_factory() { return *m_solver_factory; }
@@ -354,39 +356,40 @@ public:
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
- 
+
     void set_solver_factory(solver_factory * s);
     void set_interpolating_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
+    void complete_model();
     void validate_model();
     void display_model(model_ref& mdl);
 
-    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);    
+    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
     bool is_func_decl(symbol const & s) const;
     bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
     void insert(cmd * c);
-    void insert(symbol const & s, func_decl * f); 
+    void insert(symbol const & s, func_decl * f);
     void insert(func_decl * f) { insert(f->get_name(), f); }
     void insert(symbol const & s, psort_decl * p);
     void insert(psort_decl * p) { insert(p->get_name(), p); }
     void insert(symbol const & s, unsigned arity, sort *const* domain, expr * t);
     void insert(symbol const & s, object_ref *);
     void insert(tactic_cmd * c) { tactic_manager::insert(c); }
-    void insert(probe_info * p) { tactic_manager::insert(p); } 
-    void insert_user_tactic(symbol const & s, sexpr * d); 
+    void insert(probe_info * p) { tactic_manager::insert(p); }
+    void insert_user_tactic(symbol const & s, sexpr * d);
     void insert_aux_pdecl(pdecl * p);
     void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
     func_decl * find_func_decl(symbol const & s) const;
-    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, 
+    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                unsigned arity, sort * const * domain, sort * range) const;
     psort_decl * find_psort_decl(symbol const & s) const;
     cmd * find_cmd(symbol const & s) const;
     sexpr * find_user_tactic(symbol const & s) const;
     object_ref * find_object_ref(symbol const & s) const;
     void mk_const(symbol const & s, expr_ref & result) const;
-    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, 
+    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range,
                 expr_ref & r) const;
     void erase_cmd(symbol const & s);
     void erase_func_decl(symbol const & s);
@@ -401,7 +404,7 @@ public:
     void reset_object_refs();
     void reset_user_tactics();
     void set_regular_stream(char const * name) { m_regular.set(name); }
-    void set_diagnostic_stream(char const * name); 
+    void set_diagnostic_stream(char const * name);
     virtual std::ostream & regular_stream() { return *m_regular; }
     virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }
     char const * get_regular_stream_name() const { return m_regular.name(); }
@@ -429,7 +432,7 @@ public:
     // display the result produced by a check-sat or check-sat-using commands in the regular stream
     void display_sat_result(lbool r);
     // check if result produced by check-sat or check-sat-using matches the known status
-    void validate_check_sat_result(lbool r); 
+    void validate_check_sat_result(lbool r);
     unsigned num_scopes() const { return m_scopes.size(); }
 
     dictionary<macro_decls> const & get_macros() const { return m_macros; }
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 983dbbc78..f255c8353 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -25,11 +25,11 @@ class psort_inst_cache {
     sort *                m_const;
     obj_map<sort, void *> m_map; // if m_num_params == 1 value is a sort, otherwise it is a reference to another inst_cache
 public:
-    psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) { 
+    psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) {
     }
 
     ~psort_inst_cache() { SASSERT(m_map.empty()); SASSERT(m_const == 0); }
-    
+
     void finalize(pdecl_manager & m) {
         if (m_num_params == 0) {
             SASSERT(m_map.empty());
@@ -85,7 +85,7 @@ public:
             curr = static_cast<psort_inst_cache*>(next);
         }
     }
-    
+
     sort * find(sort * const * s) const {
         if (m_num_params == 0)
             return m_const;
@@ -138,8 +138,8 @@ class psort_sort : public psort {
     friend class pdecl_manager;
     sort * m_sort;
     psort_sort(unsigned id, pdecl_manager & m, sort * s):psort(id, 0), m_sort(s) { m.m().inc_ref(m_sort); }
-    virtual void finalize(pdecl_manager & m) { 
-        m.m().dec_ref(m_sort); 
+    virtual void finalize(pdecl_manager & m) {
+        m.m().dec_ref(m_sort);
         psort::finalize(m);
     }
     virtual bool check_num_params(pdecl * other) const { return true; }
@@ -152,7 +152,7 @@ public:
     virtual char const * hcons_kind() const { return "psort_sort"; }
     virtual unsigned hcons_hash() const { return m_sort->get_id(); }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         return m_sort == static_cast<psort_sort const *>(other)->m_sort;
     }
@@ -172,10 +172,10 @@ public:
     virtual char const * hcons_kind() const { return "psort_var"; }
     virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
-    }    
+    }
     virtual void display(std::ostream & out) const {
         out << "s_" << m_idx;
     }
@@ -197,7 +197,7 @@ class psort_app : public psort {
         DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
     }
 
-    virtual void finalize(pdecl_manager & m) { 
+    virtual void finalize(pdecl_manager & m) {
         m.lazy_dec_ref(m_decl);
         m.lazy_dec_ref(m_args.size(), m_args.c_ptr());
         psort::finalize(m);
@@ -208,14 +208,14 @@ class psort_app : public psort {
     struct khasher {
         unsigned operator()(psort_app const * d) const { return d->m_decl->hash(); }
     };
-    
+
     struct chasher {
         unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
     };
 
-    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { 
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) {
         sort * r = find(s);
-        if (r) 
+        if (r)
             return r;
         sort_ref_buffer args_i(m.m());
         unsigned sz = m_args.size();
@@ -231,11 +231,11 @@ class psort_app : public psort {
 public:
     virtual ~psort_app() {}
     virtual char const * hcons_kind() const { return "psort_app"; }
-    virtual unsigned hcons_hash() const { 
+    virtual unsigned hcons_hash() const {
         return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
     }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         if (get_num_params() != other->get_num_params())
             return false;
@@ -268,6 +268,7 @@ public:
 
 psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
     pdecl(id, num_params),
+    m_psort_kind(PSORT_BASE),
     m_name(n),
     m_inst_cache(0) {
 }
@@ -295,7 +296,7 @@ sort * psort_decl::find(sort * const * s) {
 
 #if 0
 psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
-    psort_decl(id, num_params, m, n) { 
+    psort_decl(id, num_params, m, n) {
 }
 
 void psort_dt_decl::finalize(pdecl_manager& m) {
@@ -314,9 +315,10 @@ void psort_dt_decl::display(std::ostream & out) const {
 #endif
 
 
-psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p):
+psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
     psort_decl(id, num_params, m, n),
     m_def(p) {
+    m_psort_kind = PSORT_USER;
     m.inc_ref(p);
     SASSERT(p == 0 || num_params == p->get_num_params());
 }
@@ -369,6 +371,7 @@ psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol co
     psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
     m_fid(fid),
     m_kind(k) {
+    m_psort_kind = PSORT_BUILTIN;
 }
 
 sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
@@ -417,16 +420,16 @@ void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) cons
 
 paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r):
     pdecl(id, num_params),
-    m_name(n), 
+    m_name(n),
     m_type(r) {
     if (m_type.kind() == PTR_PSORT) {
         m.inc_ref(r.get_psort());
     }
 }
 
-void paccessor_decl::finalize(pdecl_manager & m) { 
+void paccessor_decl::finalize(pdecl_manager & m) {
     if (m_type.kind() == PTR_PSORT) {
-        m.lazy_dec_ref(m_type.get_psort());	
+        m.lazy_dec_ref(m_type.get_psort());
     }
 }
 
@@ -439,7 +442,7 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const {
 }
 
 bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
-    TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; 
+    TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n";
           if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
     if (m_type.kind() != PTR_MISSING_REF)
         return true;
@@ -470,7 +473,7 @@ void paccessor_decl::display(std::ostream & out, pdatatype_decl const * const *
     out << ")";
 }
 
-pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                      symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors):
     pdecl(id, num_params),
     m_name(n),
@@ -508,7 +511,7 @@ constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, sort *
     ptr_buffer<accessor_decl> as;
     ptr_vector<paccessor_decl>::iterator it  = m_accessors.begin();
     ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
-    for (; it != end; ++it) 
+    for (; it != end; ++it)
         as.push_back((*it)->instantiate_decl(m, s));
     return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr());
 }
@@ -524,7 +527,7 @@ void pconstructor_decl::display(std::ostream & out, pdatatype_decl const * const
     out << ")";
 }
 
-pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                symbol const & n, unsigned num_constructors, pconstructor_decl * const * constructors):
     psort_decl(id, num_params, m, n),
     m_constructors(num_constructors, constructors),
@@ -641,7 +644,7 @@ void pdatatype_decl::display(std::ostream & out) const {
     out << ")";
 }
 
-pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                  unsigned num_datatypes, pdatatype_decl * const * dts):
     pdecl(id, num_params),
     m_datatypes(num_datatypes, dts) {
@@ -714,22 +717,22 @@ struct pdecl_manager::sort_info {
 
 struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
     ptr_vector<sort> m_args;
-    
+
     app_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, sort * const * s):
         sort_info(m, d),
         m_args(n, s) {
         m.m().inc_array_ref(n, s);
     }
-    
+
     virtual ~app_sort_info() {}
-    
+
     virtual unsigned obj_size() const { return sizeof(app_sort_info); }
-    
+
     virtual void finalize(pdecl_manager & m) {
         sort_info::finalize(m);
         m.m().dec_array_ref(m_args.size(), m_args.c_ptr());
     }
-    
+
     virtual void display(std::ostream & out, pdecl_manager const & m) const {
         if (m_args.empty()) {
             out << m_decl->get_name();
@@ -743,7 +746,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
             out << ")";
         }
     }
-    
+
     virtual format * pp(pdecl_manager const & m) const {
         if (m_args.empty()) {
             return mk_string(m.m(), m_decl->get_name().str().c_str());
@@ -755,7 +758,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
             return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str());
         }
     }
-}; 
+};
 
 struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
     svector<unsigned> m_indices;
@@ -781,7 +784,7 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
             out << ")";
         }
     }
-    
+
     virtual format * pp(pdecl_manager const & m) const {
         if (m_indices.empty()) {
             return mk_string(m.m(), m_decl->get_name().str().c_str());
@@ -801,7 +804,7 @@ void pdecl_manager::init_list() {
     psort * v   = mk_psort_var(1, 0);
     ptype T(v);
     ptype ListT(0);
-    paccessor_decl * as[2]    = { mk_paccessor_decl(1, symbol("head"), T), 
+    paccessor_decl * as[2]    = { mk_paccessor_decl(1, symbol("head"), T),
                                   mk_paccessor_decl(1, symbol("tail"), ListT) };
     pconstructor_decl * cs[2] = { mk_pconstructor_decl(1, symbol("nil"), symbol("is-nil"), 0, 0),
                                   mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) };
@@ -851,8 +854,8 @@ psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) {
 paccessor_decl * pdecl_manager::mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p) {
     return new (a().allocate(sizeof(paccessor_decl))) paccessor_decl(m_id_gen.mk(), num_params, *this, s, p);
 }
- 
-pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params, 
+
+pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params,
                                                         symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as) {
     return new (a().allocate(sizeof(pconstructor_decl))) pconstructor_decl(m_id_gen.mk(), num_params, *this,
                                                                            s, r, num, as);
@@ -901,9 +904,9 @@ sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args)
 
 
 void pdecl_manager::del_decl_core(pdecl * p) {
-    TRACE("pdecl_manager", 
+    TRACE("pdecl_manager",
           tout << "del_decl_core:\n";
-          if (p->is_psort()) static_cast<psort*>(p)->display(tout); 
+          if (p->is_psort()) static_cast<psort*>(p)->display(tout);
           else static_cast<psort_decl*>(p)->display(tout);
           tout << "\n";);
     size_t sz = p->obj_size();
@@ -921,7 +924,7 @@ void pdecl_manager::del_decl(pdecl * p) {
         else
             m_table.erase(_p);
     }
-    del_decl_core(p); 
+    del_decl_core(p);
 }
 
 void pdecl_manager::del_decls() {
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 2dfbb93ae..a32a42413 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -86,10 +86,13 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
 
 #define PSORT_DECL_VAR_PARAMS UINT_MAX
 
+typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind;
+
 class psort_decl : public pdecl {
 protected:
     friend class pdecl_manager;
     symbol                        m_name;
+    psort_decl_kind               m_psort_kind;
     psort_inst_cache *            m_inst_cache;
     void cache(pdecl_manager & m, sort * const * s, sort * r);
     sort * find(sort * const * s);
@@ -105,6 +108,8 @@ public:
     bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
     symbol const & get_name() const { return m_name; }
     virtual void reset_cache(pdecl_manager& m);
+    bool is_user_decl() const { return m_psort_kind == PSORT_USER; }
+    bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; }
 };
 
 class psort_user_decl : public psort_decl {
@@ -209,7 +214,7 @@ class pconstructor_decl : public pdecl {
     symbol                     m_name;
     symbol                     m_recogniser_name;
     ptr_vector<paccessor_decl> m_accessors;
-    pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+    pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                       symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors);
     virtual void finalize(pdecl_manager & m);
     virtual size_t obj_size() const { return sizeof(pconstructor_decl); }
@@ -229,7 +234,7 @@ class pdatatype_decl : public psort_decl {
     friend class pdatatypes_decl;
     ptr_vector<pconstructor_decl> m_constructors;
     pdatatypes_decl *             m_parent;
-    pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, 
+    pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n,
                    unsigned num_constructors, pconstructor_decl * const * constructors);
     virtual void finalize(pdecl_manager & m);
     virtual size_t obj_size() const { return sizeof(pdatatype_decl); }
@@ -282,7 +287,7 @@ class pdecl_manager {
     struct indexed_sort_info;
 
     obj_map<sort, sort_info *>   m_sort2info; // for pretty printing sorts
-    
+
     void init_list();
     void del_decl_core(pdecl * p);
     void del_decl(pdecl * p);
@@ -296,7 +301,7 @@ public:
     small_object_allocator & a() const { return m_allocator; }
     family_id get_datatype_fid() const { return m_datatype_fid; }
     void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; }
-    psort * mk_psort_cnst(sort * s);    
+    psort * mk_psort_cnst(sort * s);
     psort * mk_psort_var(unsigned num_params, unsigned vidx);
     psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
     psort * mk_psort_app(psort_decl * d);
diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg
index 14e83952c..58337e863 100644
--- a/src/model/model_params.pyg
+++ b/src/model/model_params.pyg
@@ -1,8 +1,9 @@
-def_module_params('model', 
+def_module_params('model',
                   export=True,
                   params=(('partial', BOOL, False, 'enable/disable partial function interpretations'),
                           ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
+                          ('completion', BOOL, False, 'enable/disable model completion'),
                           ))
 

From d61df6b91f1679a17978eb04a0e085422448f84c Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 30 Aug 2017 20:35:31 +0100
Subject: [PATCH 14/16] Model completion bug fix

---
 src/cmd_context/cmd_context.cpp | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index acbdc0bcf..aa2bb0554 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1701,9 +1701,14 @@ void cmd_context::complete_model() {
             func_decl * f = v.get_entry(i);
             if (!md->has_interpretation(f)) {
                 sort * range = f->get_range();
-                func_interp * fi = alloc(func_interp, m(), f->get_arity());
-                fi->set_else(m().get_some_value(range));
-                md->register_decl(f, fi);
+                expr * some_val = m().get_some_value(range);
+                if (f->get_arity() > 0) {
+                    func_interp * fi = alloc(func_interp, m(), f->get_arity());
+                    fi->set_else(some_val);
+                    md->register_decl(f, fi);
+                }
+                else
+                    md->register_decl(f, some_val);
             }
         }
     }

From 4d8290ebc2f5ed263b7e3499779eb32ff06f542d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 30 Aug 2017 14:04:02 -0700
Subject: [PATCH 15/16] update to theory_seq following examples from PJLJ

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/automata/automaton.h | 10 +++++
 src/smt/theory_seq.cpp        | 82 +++++++++++++++--------------------
 src/smt/theory_seq.h          |  2 +
 3 files changed, 48 insertions(+), 46 deletions(-)

diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 2f55d5cc2..12aa120b3 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -300,6 +300,16 @@ public:
         }
     }
 
+    bool is_sink_state(unsigned s) const {
+        if (is_final_state(s)) return false;
+        moves mvs;
+        get_moves_from(s, mvs);
+        for (move const& m : mvs) {
+            if (s != m.dst()) return false;
+        }
+        return true;
+    }
+
     void add_init_to_final_states() {
         add_to_final_states(init());
     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a32a4833a..44ce804e7 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -19,11 +19,12 @@ Revision History:
 --*/
 
 #include <typeinfo>
+#include "ast/ast_pp.h"
+#include "ast/ast_trail.h"
 #include "smt/proto_model/value_factory.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
 #include "smt/theory_seq.h"
-#include "ast/ast_trail.h"
 #include "smt/theory_arith.h"
 #include "smt/smt_kernel.h"
 
@@ -150,9 +151,8 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
 }
 
 void theory_seq::solution_map::display(std::ostream& out) const {
-    eqdep_map_t::iterator it = m_map.begin(), end = m_map.end();
-    for (; it != end; ++it) {
-        out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n";
+    for (auto const& kv : m_map) {
+        out << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value.first, m) << "\n";
     }
 }
 
@@ -186,9 +186,8 @@ void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) {
 }
 
 void theory_seq::exclusion_table::display(std::ostream& out) const {
-    table_t::iterator it = m_table.begin(), end = m_table.end();
-    for (; it != end; ++it) {
-        out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n";
+    for (auto const& kv : m_table) {
+        out << mk_pp(kv.first, m) << " != " << mk_pp(kv.second, m) << "\n";
     }
 }
 
@@ -213,6 +212,7 @@ theory_seq::theory_seq(ast_manager& m):
     m_trail_stack(*this),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
+    m_res(m),
     m_atoms_qhead(0),
     m_new_solution(false),
     m_new_propagation(false),
@@ -936,18 +936,14 @@ bool theory_seq::check_length_coherence0(expr* e) {
 
 bool theory_seq::check_length_coherence() {
 
-    obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
 #if 1
-    for (; it != end; ++it) {
-        expr* e = *it;
+    for (expr* e : m_length) {
         if (check_length_coherence0(e)) {
             return true;
         }
     }
-    it = m_length.begin();
 #endif
-    for (; it != end; ++it) {
-        expr* e = *it;
+    for (expr* e : m_length) {
         if (check_length_coherence(e)) {
             return true;
         }
@@ -956,10 +952,9 @@ bool theory_seq::check_length_coherence() {
 }
 
 bool theory_seq::fixed_length() {
-    obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
     bool found = false;
-    for (; it != end; ++it) {
-        if (fixed_length(*it)) {
+    for (expr* e : m_length) {
+        if (fixed_length(e)) {
             found = true;
         }
     }
@@ -2501,12 +2496,11 @@ void theory_seq::display(std::ostream & out) const {
     }
     if (!m_re2aut.empty()) {
         out << "Regex\n";
-        obj_map<expr, eautomaton*>::iterator it = m_re2aut.begin(), end = m_re2aut.end();
-        for (; it != end; ++it) {
-            out << mk_pp(it->m_key, m) << "\n";
+        for (auto const& kv : m_re2aut) {
+            out << mk_pp(kv.m_key, m) << "\n";
             display_expr disp(m);
-            if (it->m_value) {
-                it->m_value->display(out, disp);
+            if (kv.m_value) {
+                kv.m_value->display(out, disp);
             }
         }
     }
@@ -2520,9 +2514,7 @@ void theory_seq::display(std::ostream & out) const {
     }
 
     if (!m_length.empty()) {
-        obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
-        for (; it != end; ++it) {
-            expr* e = *it;
+        for (expr* e : m_length) {
             rational lo(-1), hi(-1);
             lower_bound(e, lo);
             upper_bound(e, hi);
@@ -2635,6 +2627,12 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq int.to.str", m_stats.m_int_string);
 }
 
+void theory_seq::init_search_eh() {
+    m_re2aut.reset();
+    m_res.reset();
+    m_automata.reset();
+}
+
 void theory_seq::init_model(expr_ref_vector const& es) {
     expr_ref new_s(m);
     for (expr* e : es) {
@@ -3396,7 +3394,6 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     literal lit = ctx.get_literal(n);
     if (!is_true) {
         e3 = m_util.re.mk_complement(e2);
-        is_true = true;
         lit.neg();
     }
     eautomaton* a = get_automaton(e3);
@@ -3415,26 +3412,17 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     unsigned_vector states;
     a->get_epsilon_closure(a->init(), states);
     literal_vector lits;
-    if (is_true) {
-        lits.push_back(~lit);
-    }
+    lits.push_back(~lit);
+    
     for (unsigned i = 0; i < states.size(); ++i) {
-        if (is_true) {
-            lits.push_back(mk_accept(e1, zero, e3, states[i]));
-        }
-        else {
-            literal nlit = ~lit;
-            propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i]));
-        }
+        lits.push_back(mk_accept(e1, zero, e3, states[i]));
     }
-    if (is_true) {
-        if (lits.size() == 2) {
-            propagate_lit(0, 1, &lit, lits[1]);
-        }
-        else {
-            TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
-            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-        }
+    if (lits.size() == 2) {
+        propagate_lit(0, 1, &lit, lits[1]);
+    }
+    else {
+        TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
+        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
     }
 }
 
@@ -4179,10 +4167,8 @@ eautomaton* theory_seq::get_automaton(expr* re) {
         TRACE("seq", result->display(tout, disp););
     }
     m_automata.push_back(result);
-    m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
-
     m_re2aut.insert(re, result);
-    m_trail_stack.push(insert_obj_map<theory_seq, expr, eautomaton*>(m_re2aut, re));
+    m_res.push_back(re);
     return result;
 }
 
@@ -4263,6 +4249,10 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
     if (m_util.str.is_length(idx)) return;
     SASSERT(m_autil.is_numeral(idx));
     SASSERT(get_context().get_assignment(lit) == l_true);
+    if (aut->is_sink_state(src)) {
+        propagate_lit(0, 1, &lit, false_literal);
+        return;
+    }
     bool is_final = aut->is_final_state(src);
     if (is_final == is_acc) {
         propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index b5a53e8e4..1f97697c2 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -328,6 +328,7 @@ namespace smt {
         // maintain automata with regular expressions.
         scoped_ptr_vector<eautomaton>  m_automata;
         obj_map<expr, eautomaton*>     m_re2aut;
+        expr_ref_vector                m_res;
 
         // queue of asserted atoms
         ptr_vector<expr>               m_atoms;
@@ -361,6 +362,7 @@ namespace smt {
         virtual void collect_statistics(::statistics & st) const;
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & mg);
+        virtual void init_search_eh();
 
         void init_model(expr_ref_vector const& es);
         // final check 

From 059bad909ad4b5f0b70378970475149822cccaa6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 31 Aug 2017 07:33:55 -0700
Subject: [PATCH 16/16] prune dead states from automata

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifier/base_simplifier.h |  1 +
 src/ast/simplifier/simplifier.cpp    |  9 +++-
 src/math/automata/automaton.h        | 72 +++++++++++++++++++++-------
 src/smt/asserted_formulas.cpp        |  3 +-
 src/smt/smt_quantifier.cpp           |  7 ++-
 5 files changed, 70 insertions(+), 22 deletions(-)

diff --git a/src/ast/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h
index 73a04d605..87c372636 100644
--- a/src/ast/simplifier/base_simplifier.h
+++ b/src/ast/simplifier/base_simplifier.h
@@ -37,6 +37,7 @@ protected:
                tout << mk_pp(n, m) << "\n";
                tout << mk_pp(r, m) << "\n";
                tout << mk_pp(p, m) << "\n";);
+        TRACE("cache", tout << mk_pp(n, m) << " -> " << mk_pp(r, m) << "\n";);
         SASSERT(is_rewrite_proof(n, r, p));
     }
     void reset_cache() { m_cache.reset(); }
diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp
index c02753440..e7f842203 100644
--- a/src/ast/simplifier/simplifier.cpp
+++ b/src/ast/simplifier/simplifier.cpp
@@ -591,8 +591,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 if (m_ac_cache.find(to_app(arg), new_arg)) {
                     SASSERT(new_arg != 0);
                     new_args.push_back(new_arg);
-                    if (arg != new_arg)
+                    if (arg != new_arg) {
+                        TRACE("ac", tout << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
                         has_new_arg = true;
+                    }
                     if (m.fine_grain_proofs()) {
                         proof * pr = 0;
                         m_ac_pr_cache.find(to_app(arg), pr);
@@ -610,8 +612,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 proof * pr;
                 get_cached(arg, new_arg, pr);
                 new_args.push_back(new_arg);
-                if (arg != new_arg)
+                if (arg != new_arg) {
+                    TRACE("ac", tout << "cached: " << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
                     has_new_arg = true;
+                }
                 if (m.fine_grain_proofs() && pr != 0)
                     new_arg_prs.push_back(pr);
             }
@@ -627,6 +631,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
             else {
                 app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
                 m_ac_cache.insert(curr, new_curr);
+                TRACE("ac", tout << mk_pp(curr, m) << " -> " << mk_pp(new_curr, m) << "\n";);
                 if (m.fine_grain_proofs()) {
                     proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
                     m_ac_pr_cache.insert(curr, p);
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 12aa120b3..07d6d31ec 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -25,6 +25,7 @@ Revision History:
 #include "util/util.h"
 #include "util/vector.h"
 #include "util/uint_set.h"
+#include "util/trace.h"
 
 template<class T>
 class default_value_manager {
@@ -383,12 +384,12 @@ public:
                     else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
                         moves const& mvs = m_delta[dst];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
-                            mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t()));
+                        for (move const& mv : mvs) {
+                            mvs1.push_back(move(m, src, mv.dst(), mv.t()));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
-                            remove(dst, mvs1[k].dst(), mvs1[k].t());
-                            add(mvs1[k]);
+                        for (move const& mv : mvs1) {
+                            remove(dst, mv.dst(), mv.t());
+                            add(mv);
                         }
                     }
                     //
@@ -401,13 +402,13 @@ public:
                         unsigned_vector src0s;
                         moves const& mvs = m_delta_inv[dst];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
-                            SASSERT(mvs[k].is_epsilon());
-                            mvs1.push_back(move(m, mvs[k].src(), dst1, t));
+                        for (move const& mv1 : mvs) {
+                            SASSERT(mv1.is_epsilon());
+                            mvs1.push_back(move(m, mv1.src(), dst1, t));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
-                            remove(mvs1[k].src(), dst, 0);
-                            add(mvs1[k]);
+                        for (move const& mv1 : mvs1) {
+                            remove(mv1.src(), dst, 0);
+                            add(mv1);
                         }
                         remove(dst, dst1, t);    
                         --j;
@@ -419,12 +420,12 @@ public:
                     else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
                         moves const& mvs = m_delta_inv[src];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
-                            mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
+                        for (move const& mv : mvs) {
+                            mvs1.push_back(move(m, mv.src(), dst, mv.t()));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
-                            remove(mvs1[k].src(), src, mvs1[k].t());
-                            add(mvs1[k]);
+                        for (move const& mv : mvs1) {
+                            remove(mv.src(), src, mv.t());
+                            add(mv);
                         }
                     }
                     else {
@@ -447,6 +448,7 @@ public:
                 break;
             }
         }
+        sinkify_dead_states();
     }
 
     bool is_sequence(unsigned& length) const {
@@ -564,6 +566,40 @@ public:
     }
 private:
 
+    void sinkify_dead_states() {
+        uint_set dead_states;
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            if (!m_final_states.contains(i)) {
+                dead_states.insert(i);
+            }
+        }
+        bool change = true;
+        unsigned_vector to_remove;
+        while (change) {
+            change = false;
+            to_remove.reset();
+            for (unsigned s : dead_states) {
+                moves const& mvs = m_delta[s];
+                for (move const& mv : mvs) {
+                    if (!dead_states.contains(mv.dst())) {
+                        to_remove.push_back(s);
+                        break;
+                    }
+                }
+            }
+            change = !to_remove.empty();
+            for (unsigned s : to_remove) {
+                dead_states.remove(s);
+            }
+            to_remove.reset();
+        }
+        TRACE("seq", tout << "remove: " << dead_states << "\n";);
+        for (unsigned s : dead_states) {
+            CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";); 
+            m_delta[s].reset();
+        }
+    }
+
     void remove_dead_states() {
         unsigned_vector remap;
         for (unsigned i = 0; i < m_delta.size(); ++i) {
@@ -669,8 +705,8 @@ private:
     }
 
     static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
-        for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
-            final.push_back(a.m_final_states[i]+offset);
+        for (unsigned s : a.m_final_states) {
+            final.push_back(s+offset);
         }
     }
  
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index dabae9fbd..d9630c979 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -645,7 +645,7 @@ void asserted_formulas::propagate_values() {
                 new_prs2.push_back(pr);
         }
     }
-    TRACE("propagate_values", tout << "found: " << found << "\n";);
+    TRACE("propagate_values", tout << "found: " << found << "\n" << new_exprs2 << "\n";);
     // If C is not empty, then reduce R using the updated simplifier cache with entries
     // x -> n for each constraint 'x = n' in C.
     if (found) {
@@ -656,6 +656,7 @@ void asserted_formulas::propagate_values() {
             expr_ref new_n(m);
             proof_ref new_pr(m);
             m_simplifier(n, new_n, new_pr);
+            TRACE("propagate_values", tout << mk_pp(n, m) << " -> " << new_n << "\n";);
             if (n == new_n.get()) {
                 push_assertion(n, pr, new_exprs1, new_prs1);
             }
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 84ed7c8cd..0492aff23 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -492,6 +492,7 @@ namespace smt {
 
         virtual void assign_eh(quantifier * q) {
             m_active = true;
+            ast_manager& m = m_context->get_manager();
             if (!m_fparams->m_ematching) {
                 return;
             }
@@ -514,7 +515,11 @@ namespace smt {
                 app * mp = to_app(q->get_pattern(i));
                 SASSERT(m_context->get_manager().is_pattern(mp));
                 bool unary = (mp->get_num_args() == 1);
-                if (!unary && j >= num_eager_multi_patterns) {
+                if (m.is_rec_fun_def(q) && i > 0) {
+                    // add only the first pattern
+                    TRACE("quantifier", tout << "skip recursive function body " << mk_ismt2_pp(mp, m) << "\n";);
+                }
+                else if (!unary && j >= num_eager_multi_patterns) {
                     TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
                           << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns
                           << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";);