From 4d41db3028f97748758427dcf74406658082ab81 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 Aug 2020 14:36:16 -0700
Subject: [PATCH] adding euf

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                         |  2 +-
 src/ast/euf/euf_egraph.cpp            | 14 ++---
 src/sat/sat_ddfw.h                    | 10 ++--
 src/sat/sat_drat.cpp                  | 66 +++++++++++++++++++-----
 src/sat/sat_drat.h                    | 25 ++++-----
 src/sat/sat_extension.h               |  8 +++
 src/sat/sat_lookahead.h               |  2 +-
 src/sat/sat_prob.h                    |  8 +--
 src/sat/sat_simplifier.cpp            | 17 ++++---
 src/sat/sat_solver.cpp                | 15 +++---
 src/sat/sat_solver.h                  |  1 +
 src/sat/sat_solver/inc_sat_solver.cpp |  1 +
 src/sat/smt/CMakeLists.txt            |  5 +-
 src/sat/smt/ba_solver.cpp             | 24 +++++----
 src/sat/smt/ba_solver.h               |  2 +-
 src/sat/smt/euf_internalize.cpp       | 20 +++++---
 src/sat/smt/euf_model.cpp             | 14 ++++-
 src/sat/smt/euf_proof.cpp             | 73 +++++++++++++++++++++++++++
 src/sat/smt/euf_solver.cpp            | 54 ++++++++++++++------
 src/sat/smt/euf_solver.h              | 39 ++++++++------
 src/sat/tactic/goal2sat.cpp           |  4 +-
 src/shell/main.cpp                    |  5 ++
 src/shell/opt_frontend.cpp            | 45 ++++++++++-------
 src/shell/smtlib_frontend.cpp         | 37 ++++++++++++--
 src/smt/theory_seq.cpp                | 12 -----
 src/util/mpz.h                        |  2 +-
 26 files changed, 353 insertions(+), 152 deletions(-)
 create mode 100644 src/sat/smt/euf_proof.cpp

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 30dd2a44d..9baf7660f 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -311,7 +311,7 @@ class sort_size {
     uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE
     sort_size(kind_t k, uint64_t r):m_kind(k), m_size(r) {}
 public:
-    sort_size():m_kind(SS_INFINITE) {}
+    sort_size():m_kind(SS_INFINITE), m_size(0) {}
     sort_size(uint64_t const & sz):m_kind(SS_FINITE), m_size(sz) {}
     explicit sort_size(rational const& r) {
         if (r.is_uint64()) {
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 5715447a8..4a447b44f 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -203,7 +203,6 @@ namespace euf {
         SASSERT(m_num_scopes == 0 || m_worklist.empty());
         unsigned head = 0, tail = m_worklist.size();
         while (head < tail && m.limit().inc() && !inconsistent()) {
-            TRACE("euf", tout << "iterate: " << head << " " << tail << "\n";);
             for (unsigned i = head; i < tail && !inconsistent(); ++i) {
                 enode* n = m_worklist[i]->get_root();
                 if (!n->is_marked1()) {
@@ -349,7 +348,8 @@ namespace euf {
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
         out << std::setw(5)
             << n->get_owner_id() << " := ";
-        out << n->get_root()->get_owner_id() << " ";
+        if (!n->is_root()) 
+            out << "[" << n->get_root()->get_owner_id() << "] ";
         expr* f = n->get_owner();
         if (is_app(f))
             out << to_app(f)->get_decl()->get_name() << " ";
@@ -373,10 +373,8 @@ namespace euf {
         unsigned max_args = 0;
         for (enode* n : m_nodes)
             max_args = std::max(max_args, n->num_args());
-
-        for (enode* n : m_nodes) {
+        for (enode* n : m_nodes) 
             display(out, max_args, n);          
-        }
         return out;
     }
 
@@ -397,9 +395,8 @@ namespace euf {
             enode* n1 = src.m_nodes[i];
             expr* e1 = src.m_exprs[i];
             args.reset();
-            for (unsigned j = 0; j < n1->num_args(); ++j) {
+            for (unsigned j = 0; j < n1->num_args(); ++j) 
                 args.push_back(old_expr2new_enode[n1->get_arg(j)->get_owner_id()]);
-            }
             expr*  e2 = tr(e1);
             enode* n2 = mk(e2, args.size(), args.c_ptr());
             old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
@@ -412,9 +409,8 @@ namespace euf {
             SASSERT(!n1t || n2t);
             SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner()));
             SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner()));
-            if (n1t && n2->get_root() != n2t->get_root()) {
+            if (n1t && n2->get_root() != n2t->get_root()) 
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
-            }
         }
         propagate();
     }
diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h
index 98a6873b9..411c7010c 100644
--- a/src/sat/sat_ddfw.h
+++ b/src/sat/sat_ddfw.h
@@ -90,11 +90,11 @@ namespace sat {
         indexed_uint_set m_unsat;
         indexed_uint_set m_unsat_vars;  // set of variables that are in unsat clauses
         random_gen       m_rand;
-        unsigned         m_num_non_binary_clauses;
-        unsigned         m_restart_count, m_reinit_count, m_parsync_count;
-        uint64_t         m_restart_next,  m_reinit_next,  m_parsync_next;
-        uint64_t         m_flips, m_last_flips, m_shifts;
-        unsigned         m_min_sz;
+        unsigned         m_num_non_binary_clauses{ 0 };
+        unsigned         m_restart_count{ 0 }, m_reinit_count{ 0 }, m_parsync_count{ 0 };
+        uint64_t         m_restart_next{ 0 }, m_reinit_next{ 0 }, m_parsync_next{ 0 };
+        uint64_t         m_flips{ 0 }, m_last_flips{ 0 }, m_shifts{ 0 };
+        unsigned         m_min_sz{ 0 };
         hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
         stopwatch        m_stopwatch;
 
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index d87befcf9..9062b880a 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -73,28 +73,48 @@ namespace sat {
         case drat::status::learned:  return out << "l";
         case drat::status::asserted: return out << "a";
         case drat::status::deleted:  return out << "d";
-        case drat::status::external: return out << "e";
+        case drat::status::ba:       return out << "c ba";
+        case drat::status::euf:      return out << "c euf";
         default: return out;
         }
     }
 
     void drat::dump(unsigned n, literal const* c, status st) {
-        if (st == status::asserted || st == status::external) {
+        if (st == status::asserted)
             return;
-        }
-        if (m_activity && ((m_num_add % 1000) == 0)) {
+        if (m_activity && ((m_num_add % 1000) == 0)) 
             dump_activity();
-        }
         
         char buffer[10000];
         char digits[20];     // enough for storing unsigned
         char* lastd = digits + sizeof(digits);
         
         unsigned len = 0;
-        if (st == status::deleted) {
+        switch (st) {
+        case status::deleted:
             buffer[0] = 'd';
             buffer[1] = ' ';
             len = 2;
+            break;
+        case status::euf:
+            buffer[0] = 'c';
+            buffer[1] = ' ';
+            buffer[2] = 'e';
+            buffer[3] = 'u';
+            buffer[4] = 'f';
+            buffer[5] = ' ';
+            len = 6;
+            break;
+        case status::ba:
+            buffer[0] = 'c';
+            buffer[1] = ' ';
+            buffer[2] = 'b';
+            buffer[3] = 'a';
+            buffer[4] = ' ';
+            len = 5;
+            break;
+        default:
+            break;
         }
         for (unsigned i = 0; i < n; ++i) {
             literal lit = c[i];
@@ -133,7 +153,8 @@ namespace sat {
         unsigned char ch = 0;
         switch (st) {
         case status::asserted: return;
-        case status::external: return; 
+        case status::ba: return; 
+        case status::euf: return; 
         case status::learned: ch = 'a'; break;
         case status::deleted: ch = 'd'; break;
         default: UNREACHABLE(); break;
@@ -237,6 +258,27 @@ namespace sat {
         }
     }
 
+    void drat::bool_def(bool_var v, unsigned n) {
+        if (m_out)
+            (*m_out) << "bool " << v << " := " << n << "\n";
+    }
+
+    void drat::def_begin(unsigned n, symbol const& name) {
+        if (m_out) 
+            (*m_out) << "def " << n << " := " << name;
+    }
+
+    void drat::def_add_arg(unsigned arg) {
+        if (m_out) 
+            (*m_out) << " " << arg;
+    }
+
+    void drat::def_end() {
+        if (m_out) 
+            (*m_out) << "\n";
+    }
+
+
 #if 0
     // debugging code
     bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) {
@@ -439,7 +481,7 @@ namespace sat {
         SASSERT(lits.size() == n);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             status st = m_status[i];
-            if (m_proof[i] && m_proof[i]->size() > 1 && (st == status::asserted || st == status::external)) {
+            if (m_proof[i] && m_proof[i]->size() > 1 && st == status::asserted) {
                 clause& c = *m_proof[i];
                 unsigned j = 0;
                 for (; j < c.size() && c[j] != ~l; ++j) {}
@@ -698,15 +740,15 @@ namespace sat {
             append(*cl, get_status(learned));
         }
     }
-    void drat::add(literal_vector const& lits, svector<premise> const& premises) {
+    void drat::add(literal_vector const& lits, status th) {
         ++m_num_add;
         if (m_check) {
             switch (lits.size()) {
             case 0: add(); break;
-            case 1: append(lits[0], status::external); break;
+            case 1: append(lits[0], th); break;
             default: {
                 clause* c = m_alloc.mk_clause(lits.size(), lits.c_ptr(), true);
-                append(*c, status::external);
+                append(*c, th);
                 break;
             }
             }
@@ -724,7 +766,7 @@ namespace sat {
             default: {
                 verify(c.size(), c.begin());
                 clause* cl = m_alloc.mk_clause(c.size(), c.c_ptr(), true);
-                append(*cl, status::external);                
+                append(*cl, status::ba);                
                 break;
             }
             }
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 8c32e3881..c7a1caf03 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -21,20 +21,8 @@ Notes:
 namespace sat {
     class drat {
     public:
-        struct s_ext {};
-        struct s_unit {};
-        struct premise {
-            enum { t_clause, t_unit, t_ext } m_type;
-            union {
-                clause* m_clause;
-                unsigned m_literal;                
-            };
-            premise(s_ext, literal l): m_type(t_ext), m_literal(l.index()) {}
-            premise(s_unit, literal l): m_type(t_unit), m_literal(l.index()) {}
-            premise(clause* c): m_type(t_clause), m_clause(c) {}
-        };
+        enum status { asserted, learned, deleted, ba, euf };
     private:
-        enum status { asserted, learned, deleted, external };
         struct watched_clause {
             clause* m_clause;
             literal m_l1, m_l2;
@@ -91,9 +79,18 @@ namespace sat {
         void add(literal l, bool learned);
         void add(literal l1, literal l2, bool learned);
         void add(clause& c, bool learned);
-        void add(literal_vector const& c, svector<premise> const& premises);
+        void add(literal_vector const& c, status st);
         void add(literal_vector const& c); // add learned clause
 
+        // support for SMT - connect Boolean variables with AST nodes
+        // associate AST node id with Boolean variable v
+        void bool_def(bool_var v, unsigned n);
+
+        // declare AST node n with 'name' and arguments arg
+        void def_begin(unsigned n, symbol const& name);
+        void def_add_arg(unsigned arg);
+        void def_end();
+
         bool is_cleaned(clause& c) const;        
         void del(literal l);
         void del(literal l1, literal l2);
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 884a49986..dac8ec8d1 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -45,6 +45,12 @@ namespace sat {
         ext_constraint_list & get(literal l) { return m_use_list[l.index()]; }
         ext_constraint_list const & get(literal l) const { return m_use_list[l.index()]; }
         void finalize() { m_use_list.finalize(); }
+        bool contains(bool_var v) const {
+            if (m_use_list.size() <= 2*v)
+                return false;
+            literal lit(v, false);
+            return !get(lit).empty() || !get(~lit).empty();
+        }
     };
 
     class extension {
@@ -53,7 +59,9 @@ namespace sat {
         virtual unsigned get_id() const { return 0; }
         virtual void set_solver(solver* s) = 0;
         virtual void set_lookahead(lookahead* s) = 0;
+        virtual void init_search() {}
         virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
+        virtual bool is_external(bool_var v) = 0;
         virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
         virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 55292b5ad..1be2e91d5 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -524,7 +524,7 @@ namespace sat {
         void update_lookahead_reward(literal l, unsigned level);
         bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; }
         void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; }
-        bool dl_no_overflow(unsigned base) const { return base + 2 * m_lookahead.size() * static_cast<uint64_t>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; }
+        bool dl_no_overflow(unsigned base) const { return base + static_cast < uint64_t>(2 * m_lookahead.size()) * static_cast <uint64_t>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; }
 
         unsigned do_double(literal l, unsigned& base);
         unsigned double_look(literal l, unsigned& base);
diff --git a/src/sat/sat_prob.h b/src/sat/sat_prob.h
index c29667bbe..1b3184f44 100644
--- a/src/sat/sat_prob.h
+++ b/src/sat/sat_prob.h
@@ -59,7 +59,7 @@ namespace sat {
         clause_vector    m_clause_db;     
         svector<clause_info> m_clauses;
         bool_vector    m_values, m_best_values;
-        unsigned         m_best_min_unsat;
+        unsigned         m_best_min_unsat{ 0 };
         vector<unsigned_vector> m_use_list;
         unsigned_vector  m_flat_use_list;
         unsigned_vector  m_use_list_index;
@@ -68,9 +68,9 @@ namespace sat {
         indexed_uint_set m_unsat;
         random_gen       m_rand;
         unsigned_vector  m_breaks;
-        uint64_t         m_flips;
-        uint64_t         m_next_restart;
-        unsigned         m_restart_count;
+        uint64_t         m_flips{ 0 };
+        uint64_t         m_next_restart{ 0 };
+        unsigned         m_restart_count{ 0 };
         stopwatch        m_stopwatch;
         model            m_model;
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 3b3a18e80..6bf3a92f9 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -76,12 +76,17 @@ namespace sat {
     watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
 
     bool simplifier::is_external(bool_var v) const { 
-        return 
-            s.is_assumption(v) ||
-            (s.is_external(v) && s.is_incremental()) ||
-            (s.is_external(v) && s.m_ext &&
-             (!m_ext_use_list.get(literal(v, false)).empty() ||
-              !m_ext_use_list.get(literal(v, true)).empty()));
+        if (!s.is_external(v))
+            return s.is_assumption(v);
+        if (s.is_incremental())
+            return true;
+        if (!s.m_ext)
+            return false;
+        if (s.m_ext->is_external(v))
+            return true;
+        if (m_ext_use_list.contains(v))
+            return true;
+        return false;
     }
 
     inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0a036e849..626ed823b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1843,6 +1843,8 @@ namespace sat {
         m_min_core.reset();
         m_simplifier.init_search();
         m_mc.init_search(*this);
+        if (m_ext)
+            m_ext->init_search();
         TRACE("sat", display(tout););
     }
 
@@ -2983,16 +2985,15 @@ namespace sat {
             level = update_max_level(js.get_literal2(), level, unique_max);
             return level;
         case justification::CLAUSE: 
-            for (literal l : get_clause(js)) {
+            for (literal l : get_clause(js)) 
                 level = update_max_level(l, level, unique_max);
-            }
             return level;
-        case justification::EXT_JUSTIFICATION: 
-            SASSERT(not_l != null_literal);
-            fill_ext_antecedents(~not_l, js);
-            for (literal l : m_ext_antecedents) {
+        case justification::EXT_JUSTIFICATION:
+            if (not_l != null_literal) 
+                not_l.neg();
+            fill_ext_antecedents(not_l, js);
+            for (literal l : m_ext_antecedents) 
                 level = update_max_level(l, level, unique_max);
-            }
             return level;
         default:
             UNREACHABLE();
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index a4f42fdb6..17fa4ca20 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -397,6 +397,7 @@ namespace sat {
         void set_par(parallel* p, unsigned id);
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
+        drat& get_drat() { return m_drat; }
         void set_incremental(bool b) { m_config.m_incremental = b; }
         bool is_incremental() const { return m_config.m_incremental; }
         extension* get_extension() const override { return m_ext.get(); }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 378e114b4..bc8170183 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -973,6 +973,7 @@ private:
         if (m_sat_mc) {
             (*m_sat_mc)(mdl);
         }
+        m_goal2sat.update_model(mdl);
         if (m_mcs.back()) {      
             TRACE("sat", m_mcs.back()->display(tout););
             (*m_mcs.back())(mdl);
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index c990f47b4..e695de0b8 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -1,13 +1,14 @@
 z3_add_component(sat_smt
   SOURCES
     atom2bool_var.cpp
+    ba_internalize.cpp
     ba_solver.cpp
     xor_solver.cpp
-    ba_internalize.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
-    euf_solver.cpp
     euf_model.cpp
+    euf_proof.cpp
+    euf_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index 563181725..cf67253fe 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -317,14 +317,6 @@ namespace sat {
             m_num_propagations_since_pop++;
             //TRACE("ba", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
             SASSERT(validate_unit_propagation(c, lit));
-            if (get_config().m_drat) {
-                svector<drat::premise> ps;
-                literal_vector lits;
-                get_antecedents(lit, c, lits);
-                lits.push_back(lit);
-                ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
-                drat_add(lits, ps);
-            }
             assign(lit, justification::mk_ext_justification(s().scope_lvl(), c.cindex()));
             break;
         }
@@ -1604,9 +1596,8 @@ namespace sat {
 
         TRACE("ba", tout << m_lemma << "\n";);
 
-        if (get_config().m_drat) {
-            svector<drat::premise> ps; // TBD fill in
-            drat_add(m_lemma, ps);
+        if (get_config().m_drat && m_solver) {
+            s().m_drat.add(m_lemma, sat::drat::status::ba);
         }
 
         s().m_lemma.reset();
@@ -1843,6 +1834,10 @@ namespace sat {
         add_pb_ge(lit, wlits, k, m_is_redundant);
     }
 
+    bool ba_solver::is_external(bool_var v) {
+        return false;
+    }
+
     /*
       \brief return true to keep watching literal.
     */
@@ -2129,6 +2124,13 @@ namespace sat {
         case xr_t: get_antecedents(l, c.to_xr(), r); break;
         default: UNREACHABLE(); break;
         }
+        if (get_config().m_drat && m_solver) {
+            literal_vector lits;
+            for (literal lit : r) 
+                lits.push_back(~lit);
+            lits.push_back(l);
+            s().m_drat.add(lits, sat::drat::status::ba);
+        }
     }
 
     void ba_solver::nullify_tracking_literal(constraint& c) {
diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h
index 48cb96356..ecc06d3c2 100644
--- a/src/sat/smt/ba_solver.h
+++ b/src/sat/smt/ba_solver.h
@@ -469,7 +469,6 @@ namespace sat {
             else m_solver->set_conflict(j, l); 
         }
         inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
-        inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { if (m_solver) m_solver->m_drat.add(c, premises); }
 
 
         mutable bool m_overflow;
@@ -572,6 +571,7 @@ namespace sat {
         void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void add_xr(literal_vector const& lits);
 
+        bool is_external(bool_var v) override;
         bool propagate(literal l, ext_constraint_idx idx) override;
         lbool resolve_conflict() override;
         void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 54b8210af..727d3a806 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -54,7 +54,7 @@ namespace euf {
             m_args.reset();
             for (unsigned i = 0; i < num; ++i)
                 m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
-            if (root && internalize_root(to_app(e), m_args.c_ptr(), sign))
+            if (root && internalize_root(to_app(e), sign))
                 return sat::null_literal;
             n = m_egraph.mk(e, num, m_args.c_ptr());
             attach_node(n);
@@ -90,8 +90,10 @@ namespace euf {
 
     void solver::attach_node(euf::enode* n) {
         expr* e = n->get_owner();
+        log_node(n);
         if (m.is_bool(e)) {
             sat::bool_var v = si.add_bool_var(e);
+            log_bool_var(v, n);
             attach_lit(literal(v, false),  n);
         }
         axiomatize_basic(n);
@@ -112,12 +114,13 @@ namespace euf {
         m_var_trail.push_back(v);
     }
 
-    bool solver::internalize_root(app* e, enode* const* args, bool sign) {
+    bool solver::internalize_root(app* e, bool sign) {
         if (m.is_distinct(e)) {
+            enode_vector _args(m_args);
             if (sign)
-                add_not_distinct_axiom(e, args);
+                add_not_distinct_axiom(e, _args.c_ptr());
             else
-                add_distinct_axiom(e, args);
+                add_distinct_axiom(e, _args.c_ptr());
             return true;
         }
         return false;
@@ -129,7 +132,7 @@ namespace euf {
         if (sz <= 1)
             return;
 
-        static const unsigned distinct_max_args = 24;
+        static const unsigned distinct_max_args = 32;
         if (sz <= distinct_max_args) {
             sat::literal_vector lits;
             for (unsigned i = 0; i < sz; ++i) {
@@ -157,19 +160,19 @@ namespace euf {
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq(m.mk_eq(gapp, arg), m);
                 sat::literal lit = internalize(eq, false, false, m_is_redundant);
-                s().add_clause(1, &lit, false);
+                s().add_clause(1, &lit, m_is_redundant);
                 eqs.push_back(m.mk_eq(fapp, a));
             }
             pb_util pb(m);
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.c_ptr(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
-            s().mk_clause(1, &lit, false);
+            s().mk_clause(1, &lit, m_is_redundant);
         }
     }
 
     void solver::add_distinct_axiom(app* e, enode* const* args) {
         SASSERT(m.is_distinct(e));
-        static const unsigned distinct_max_args = 24;
+        static const unsigned distinct_max_args = 32;
         unsigned sz = e->get_num_args();
         if (sz <= 1) {
             s().mk_clause(0, nullptr, m_is_redundant);
@@ -211,6 +214,7 @@ namespace euf {
             expr* el = a->get_arg(2);
             sat::bool_var v = m_expr2var.to_bool_var(c);
             SASSERT(v != sat::null_bool_var);
+            SASSERT(!m.is_bool(e));
             expr_ref eq_th(m.mk_eq(a, th), m);
             expr_ref eq_el(m.mk_eq(a, el), m);
             sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant);
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 115fe944b..95ae940c5 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -69,7 +69,19 @@ namespace euf {
             }
             // model of s() must have been fixed.
             if (m.is_bool(e)) {
-                switch (s().value(m_expr2var.to_bool_var(e))) {
+                if (m.is_true(e)) {
+                    values.set(id, m.mk_true());
+                    continue;
+                }
+                if (m.is_false(e)) {
+                    values.set(id, m.mk_false());
+                    continue;
+                }
+                if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
+                    continue;
+                sat::bool_var v = m_expr2var.to_bool_var(e);
+                SASSERT(v != sat::null_bool_var);
+                switch (s().value(v)) {
                 case l_true:
                     values.set(id, m.mk_true());
                     break;
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
new file mode 100644
index 000000000..0ed4a965f
--- /dev/null
+++ b/src/sat/smt/euf_proof.cpp
@@ -0,0 +1,73 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_proof.cpp
+
+Abstract:
+
+    Proof logging facilities.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+
+#include "sat/smt/euf_solver.h"
+
+namespace euf {
+
+    void solver::log_node(enode* n) {
+        if (m_drat) {
+            expr* e = n->get_owner();
+            if (is_app(e)) {
+                symbol const& name = to_app(e)->get_name();
+                s().get_drat().def_begin(n->get_owner_id(), name);
+                for (enode* arg : enode_args(n)) {
+                    s().get_drat().def_add_arg(arg->get_owner_id());
+                }
+                s().get_drat().def_end();
+            }
+            else {
+                IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
+            }
+        }
+    }
+
+    void solver::log_bool_var(sat::bool_var v, enode* n) {
+        if (m_drat) {
+            s().get_drat().bool_def(v, n->get_owner_id());
+        }
+    }
+
+    void solver::log_antecedents(literal l, literal_vector const& r) {
+        TRACE("euf", log_antecedents(tout, l, r););
+        if (m_drat) {
+            literal_vector lits;
+            for (literal lit : r) lits.push_back(~lit);
+            if (l != sat::null_literal)
+                lits.push_back(l);
+            s().get_drat().add(lits, sat::drat::status::euf);
+        }
+    }
+
+    void solver::log_antecedents(std::ostream& out, literal l, literal_vector const& r) {
+        for (sat::literal l : r) {
+            enode* n = m_var2node[l.var()];
+            out << ~l << ": ";
+            if (!l.sign()) out << "! ";
+            out << mk_pp(n->get_owner(), m) << "\n";
+            SASSERT(s().value(l) == l_true);
+        }
+        if (l != sat::null_literal) {
+            out << l << ": ";
+            if (l.sign()) out << "! ";
+            enode* n = m_var2node[l.var()];
+            out << mk_pp(n->get_owner(), m) << "\n";            
+        }
+    }
+
+
+}
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 2c6e1231f..f588eca8e 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -16,6 +16,7 @@ Author:
 --*/
 
 #include "ast/pb_decl_plugin.h"
+#include "ast/ast_ll_pp.h"
 #include "sat/sat_solver.h"
 #include "sat/smt/sat_smt.h"
 #include "sat/smt/ba_solver.h"
@@ -25,6 +26,7 @@ namespace euf {
 
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
+        m_drat = s().get_config().m_drat;
     }
 
     /**
@@ -82,6 +84,19 @@ namespace euf {
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
+    void solver::init_search() {
+        TRACE("euf", display(tout););
+    }
+
+    bool solver::is_external(bool_var v) {
+        if (nullptr != m_var2node.get(v, nullptr))
+            return true;
+        for (auto* s : m_solvers)
+            if (s->is_external(v))
+                return true;
+        return false;
+    }
+
     bool solver::propagate(literal l, ext_constraint_idx idx) { 
         force_push();
         auto* ext = sat::constraint_base::to_extension(idx);
@@ -127,6 +142,8 @@ namespace euf {
         }
         for (unsigned* idx : m_explain) 
             r.push_back(sat::to_literal((unsigned)(idx - base_ptr())));
+
+        log_antecedents(l, r);
     }
 
     void solver::asserted(literal l) {
@@ -145,12 +162,12 @@ namespace euf {
         if (m.is_eq(e) && !sign) {
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
-            TRACE("euf", tout << "merge " << na->get_owner_id() << nb->get_owner_id() << "\n";);
+            TRACE("euf", tout << mk_pp(e, m) << "\n";);
             m_egraph.merge(na, nb, base_ptr() + l.index());
         }
         else {            
             euf::enode* nb = sign ? mk_false() : mk_true();
-            TRACE("euf", tout << "merge " << n->get_owner_id() << " " << mk_pp(nb->get_owner(), m)  << "\n";);
+            TRACE("euf", tout << (sign ? "not ": " ") << mk_pp(n->get_owner(), m)  << "\n";);
             m_egraph.merge(n, nb, base_ptr() + l.index());
         }
         // TBD: delay propagation?
@@ -159,8 +176,10 @@ namespace euf {
 
     void solver::propagate() {     
         m_egraph.propagate();
-        if (m_egraph.inconsistent()) {       
-            s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), conflict_constraint().to_index()));
+        unsigned lvl = s().scope_lvl();
+
+        if (m_egraph.inconsistent()) {  
+            s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
             return;
         }
         for (euf::enode* eq : m_egraph.new_eqs()) {
@@ -168,7 +187,10 @@ namespace euf {
             expr* a = nullptr, *b = nullptr;
             if (s().value(v) == l_false && m_ackerman && m.is_eq(eq->get_owner(), a, b))
                 m_ackerman->cg_conflict_eh(a, b);
-            s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), eq_constraint().to_index()));
+            literal lit(v, false);
+            if (s().value(lit) == l_true)
+                continue;
+            s().assign(literal(v, false), sat::justification::mk_ext_justification(lvl, eq_constraint().to_index()));
         }
         for (euf::enode* p : m_egraph.new_lits()) {
             expr* e = p->get_owner();
@@ -177,9 +199,11 @@ namespace euf {
             SASSERT(m.is_true(p->get_root()->get_owner()) || sign);
             bool_var v = m_expr2var.to_bool_var(e);
             literal lit(v, sign);
+            if (s().value(lit) == l_true)
+                continue;
             if (s().value(lit) == l_false && m_ackerman) 
                 m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner());
-            s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), lit_constraint().to_index()));
+            s().assign(lit, sat::justification::mk_ext_justification(lvl, lit_constraint().to_index()));
         }
     }
 
@@ -218,14 +242,14 @@ namespace euf {
     }
 
     void solver::push() {
-		scope s;
-		s.m_var_lim = m_var_trail.size();
-		s.m_trail_lim = m_trail.size();
-		m_scopes.push_back(s);
-		m_region.push_scope();
-		for (auto* e : m_solvers)
-			e->push();
-		m_egraph.push();
+        scope s;
+        s.m_var_lim = m_var_trail.size();
+        s.m_trail_lim = m_trail.size();
+        m_scopes.push_back(s);
+        m_region.push_scope();
+        for (auto* e : m_solvers)
+            e->push();
+        m_egraph.push();
     }
 
     void solver::force_push() {
@@ -281,7 +305,7 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             euf::enode* n = m_var2node[v];
-            out << v << ": " << m_egraph.pp(n);
+            out << v << ": " << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index afcd9187a..9ddcfc3bd 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -66,6 +66,7 @@ namespace euf {
         atom2bool_var&        m_expr2var;
         sat::sat_internalizer& si;
         smt_params            m_config;
+        bool                  m_drat { false };
         euf::egraph           m_egraph;
         stats                 m_stats;
         region                m_region;
@@ -104,7 +105,7 @@ namespace euf {
         void add_distinct_axiom(app* e, euf::enode* const* args);
         void add_not_distinct_axiom(app* e, euf::enode* const* args);
         void axiomatize_basic(enode* n);
-        bool internalize_root(app* e, enode* const* args, bool sign);
+        bool internalize_root(app* e, bool sign);
         euf::enode* mk_true();
         euf::enode* mk_false();
 
@@ -127,6 +128,10 @@ namespace euf {
         void propagate();
         void get_antecedents(literal l, constraint& j, literal_vector& r);
         void force_push();
+        void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
+        void log_antecedents(literal l, literal_vector const& r);
+        void log_node(enode* n);
+        void log_bool_var(sat::bool_var v, enode* n);
 
         constraint& mk_constraint(constraint*& c, constraint::kind_t k);
         constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
@@ -155,26 +160,28 @@ namespace euf {
            if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
        }
 
+       struct scoped_set_translate {
+           solver& s;
+           scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
+               s(s) {
+               s.m_to_m = &m;
+               s.m_to_expr2var = &a2b;
+               s.m_to_si = &si;
+           }
+           ~scoped_set_translate() {
+               s.m_to_m = &s.m;
+               s.m_to_expr2var = &s.m_expr2var;
+               s.m_to_si = &s.si;
+           }
+       };
+
         void updt_params(params_ref const& p);
         void set_solver(sat::solver* s) override { m_solver = s; }
         void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
-        struct scoped_set_translate {
-            solver& s;
-            scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
-                s(s) { 
-                s.m_to_m = &m; 
-                s.m_to_expr2var = &a2b; 
-                s.m_to_si = &si; 
-            }
-            ~scoped_set_translate() { 
-                s.m_to_m = &s.m; 
-                s.m_to_expr2var = &s.m_expr2var; 
-                s.m_to_si = &s.si;  
-            }
-        };
-
+        void init_search() override;
         double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
         bool is_extended_binary(ext_justification_idx idx, literal_vector& r) override;
+        bool is_external(bool_var v) override;
         bool propagate(literal l, ext_constraint_idx idx) override;
         void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
         void asserted(literal l) override;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 8b26587d9..4d176b054 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -433,7 +433,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void convert_iff2(app * t, bool root, bool sign) {
         SASSERT(t->get_num_args() == 2);
-        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
         sat::literal  l1 = m_result_stack[sz-1];
@@ -467,7 +466,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void convert_iff(app * t, bool root, bool sign) {
-        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
         if (!m_euf && is_xor(t))
             convert_ba(t, root, sign);
         else               
@@ -678,7 +676,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     
     void process(expr * n) {
         m_result_stack.reset();
-        TRACE("goal2sat", tout << mk_pp(n, m) << "\n";);
+        TRACE("goal2sat", tout << "assert: "<< mk_pp(n, m) << "\n";);
         process(n, true, m_is_redundant);
         CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 36eb92a6d..bee73fb25 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -50,6 +50,7 @@ static char const * g_input_file          = nullptr;
 static bool         g_standard_input      = false;
 static input_kind   g_input_kind          = IN_UNSPECIFIED;
 bool                g_display_statistics  = false;
+bool                g_display_model       = false;
 static bool         g_display_istatistics = false;
 
 static void error(const char * msg) {
@@ -84,6 +85,7 @@ void display_usage() {
     std::cout << "  -lp         use parser for a modest subset of CPLEX LP input format.\n";
     std::cout << "  -log        use parser for Z3 log input format.\n";
     std::cout << "  -in         read formula from standard input.\n";
+    std::cout << "  -model      display model for satisfiable SMT.\n";
     std::cout << "\nMiscellaneous:\n";
     std::cout << "  -h, -?      prints this message.\n";
     std::cout << "  -version    prints version number of Z3.\n";
@@ -208,6 +210,9 @@ static void parse_cmd_line_args(int argc, char ** argv) {
                 g_display_statistics = true; 
                 gparams::set("stats", "true");
             }
+            else if (strcmp(opt_name, "model") == 0) {
+                g_display_model = true;
+            }
             else if (strcmp(opt_name, "ist") == 0) {
                 g_display_istatistics = true; 
             }
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index b4e2b3f3b..bf59b8cea 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -22,32 +22,40 @@ Copyright (c) 2015 Microsoft Corporation
 #include "opt/opt_parse.h"
 
 extern bool g_display_statistics;
+extern bool g_display_model;
 static bool g_first_interrupt = true;
 static opt::context* g_opt = nullptr;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
 static mutex *display_stats_mux = new mutex;
 
+static void display_model(std::ostream& out) {
+    if (!g_opt)
+        return;
+    model_ref mdl;
+    g_opt->get_model(mdl);
+    if (mdl) {
+        model_smt2_pp(out, g_opt->get_manager(), *mdl, 0); 
+    }
+    for (unsigned h : g_handles) {
+        expr_ref lo = g_opt->get_lower(h);
+        expr_ref hi = g_opt->get_upper(h);
+        if (lo == hi) {
+            out << "   " << lo << "\n";
+        }
+        else {
+            out << "  [" << lo << ":" << hi << "]\n";
+        }
+    }
+}
+
+static void display_model() {
+    if (g_display_model)
+        display_model(std::cout);
+}
 
 static void display_results() {
-    IF_VERBOSE(1, 
-               if (g_opt) {
-                   model_ref mdl;
-                   g_opt->get_model(mdl);
-                   if (mdl) {
-                       model_smt2_pp(verbose_stream(), g_opt->get_manager(), *mdl, 0); 
-                   }
-                   for (unsigned h : g_handles) {
-                       expr_ref lo = g_opt->get_lower(h);
-                       expr_ref hi = g_opt->get_upper(h);
-                       if (lo == hi) {
-                           std::cout << "   " << lo << "\n";
-                       }
-                       else {
-                           std::cout << "  [" << lo << ":" << hi << "]\n";
-                       }
-                   }
-               });
+    IF_VERBOSE(1, display_model(verbose_stream()));
 }
 
 static void display_statistics() {
@@ -128,6 +136,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
         std::cerr << ex.msg() << "\n";
     }
     display_statistics();
+    display_model();
     g_opt = nullptr;
     return 0;
 }
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 5f2b1e3dc..f63b0f2df 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -35,6 +35,7 @@ Revision History:
 static mutex *display_stats_mux = new mutex;
 
 extern bool g_display_statistics;
+extern bool g_display_model;
 static clock_t             g_start_time;
 static cmd_context *       g_cmd_context = nullptr;
 
@@ -51,6 +52,14 @@ static void display_statistics() {
     }
 }
 
+static void display_model() {
+    if (g_display_model && g_cmd_context) {
+        model_ref mdl;
+        if (g_cmd_context->is_model_available(mdl))
+            g_cmd_context->display_model(mdl);
+    }
+}
+
 static void on_timeout() {
     display_statistics();
     exit(0);    
@@ -63,10 +72,19 @@ static void STD_CALL on_ctrl_c(int) {
 }
 
 void help_tactics() {
+    struct cmp {
+        bool operator()(tactic_cmd* a, tactic_cmd* b) const {
+            return a->get_name().str() < b->get_name().str();
+        }
+    };
     cmd_context ctx;
-    for (auto cmd : ctx.tactics()) {
+    ptr_vector<tactic_cmd> cmds;
+    for (auto cmd : ctx.tactics()) 
+        cmds.push_back(cmd);
+    cmp lt;
+    std::sort(cmds.begin(), cmds.end(), lt);
+    for (auto cmd : cmds) 
         std::cout << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
-    }
 }
 
 void help_tactic(char const* name) {
@@ -82,10 +100,19 @@ void help_tactic(char const* name) {
 }
 
 void help_probes() {
+    struct cmp {
+        bool operator()(probe_info* a, probe_info* b) const {
+            return a->get_name().str() < b->get_name().str();
+        }
+    };
     cmd_context ctx;
-    for (auto cmd : ctx.probes()) {
+    ptr_vector<probe_info> cmds;
+    for (auto cmd : ctx.probes()) 
+        cmds.push_back(cmd);
+    cmp lt;
+    std::sort(cmds.begin(), cmds.end(), lt);
+    for (auto cmd : cmds) 
         std::cout << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
-    }
 }
 
 unsigned read_smtlib2_commands(char const * file_name) {
@@ -118,8 +145,8 @@ unsigned read_smtlib2_commands(char const * file_name) {
         result = parse_smt2_commands(ctx, std::cin, true);
     }
 
-
     display_statistics();
+    display_model();
     g_cmd_context = nullptr;
     return result ? 0 : 1;
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 868f4f9bf..077e83284 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -318,7 +318,6 @@ struct scoped_enable_trace {
 };
 
 final_check_status theory_seq::final_check_eh() {
-    force_push();
     if (!m_has_seq) {
         return FC_DONE;
     }
@@ -1493,7 +1492,6 @@ bool theory_seq::internalize_atom(app* a, bool) {
 }
 
 bool theory_seq::internalize_term(app* term) {
-    force_push();
     m_has_seq = true;
     if (ctx.e_internalized(term)) {
         enode* e = ctx.get_enode(term);
@@ -1621,7 +1619,6 @@ bool theory_seq::check_int_string(expr* e) {
     
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
-    force_push();
     mk_var(n);
 }
 
@@ -2521,7 +2518,6 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
 
 
 void theory_seq::propagate() {
-    force_push();
     if (ctx.get_fparams().m_seq_use_unicode)
         m_unicode.propagate();
     if (m_regex.can_propagate())
@@ -2913,7 +2909,6 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
 }
 
 void theory_seq::assign_eh(bool_var v, bool is_true) {
-    force_push();
     expr* e = ctx.bool_var2expr(v);
     expr* e1 = nullptr, *e2 = nullptr;
     expr_ref f(m);
@@ -3029,7 +3024,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
 }
 
 void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
-    force_push();
     enode* n1 = get_enode(v1);
     enode* n2 = get_enode(v2);
     expr* o1 = n1->get_owner();
@@ -3073,7 +3067,6 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
 }
 
 void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
-    force_push();
     enode* n1 = get_enode(v1);
     enode* n2 = get_enode(v2);    
     expr_ref e1(n1->get_owner(), m);
@@ -3109,8 +3102,6 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
 }
 
 void theory_seq::push_scope_eh() {
-    if (lazy_push()) 
-        return;
     theory::push_scope_eh();
     m_rep.push_scope();
     m_exclude.push_scope();
@@ -3125,8 +3116,6 @@ void theory_seq::push_scope_eh() {
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
-    if (lazy_pop(num_scopes))
-        return;
     m_trail_stack.pop_scope(num_scopes);
     theory::pop_scope_eh(num_scopes);
     m_dm.pop_scope(num_scopes);
@@ -3148,7 +3137,6 @@ void theory_seq::restart_eh() {
 }
 
 void theory_seq::relevant_eh(app* n) {
-    force_push();
     if (m_util.str.is_index(n)   ||
         m_util.str.is_replace(n) ||
         m_util.str.is_extract(n) ||
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 28fa2880b..ebfe98704 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -107,7 +107,7 @@ public:
     }
 
     mpz& operator=(mpz const& other) = delete;
-    mpz& operator=(mpz &&other) {
+    mpz& operator=(mpz &&other) noexcept {
         swap(other);
         return *this;
     }