merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-24 17:45:32 +00:00 · 2021-05-03 12:41:14 -07:00 · 2021-05-03 12:41:14 -07:00 · dc879dc3fb
commit dc879dc3fb
parent f7e476a4a0 0c6722f48b
74 changed files with 585 additions and 259 deletions
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@ -335,6 +335,7 @@ namespace z3 {
        expr bool_const(char const * name);
        expr int_const(char const * name);
        expr real_const(char const * name);
+        expr string_const(char const * name);
        expr bv_const(char const * name, unsigned sz);
        expr fpa_const(char const * name, unsigned ebits, unsigned sbits);

@ -497,6 +498,7 @@ namespace z3 {
        ast(context & c):object(c), m_ast(0) {}
        ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
        ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
+        ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
        ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
        operator Z3_ast() const { return m_ast; }
        operator bool() const { return m_ast != 0; }
@ -508,6 +510,12 @@ namespace z3 {
            m_ast = s.m_ast;
            return *this;
        }
+        ast & operator=(ast && s) noexcept {
+            object::operator=(std::forward<object>(s));
+            m_ast = s.m_ast;
+            s.m_ast = nullptr;
+            return *this;
+        }
        Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
        unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
        friend std::ostream & operator<<(std::ostream & out, ast const & n);
@ -568,7 +576,6 @@ namespace z3 {
            unsigned m_index;
        public:
            iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
-            iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}

            bool operator==(iterator const& other) const noexcept {
                return other.m_index == m_index;
@ -864,6 +871,36 @@ namespace z3 {
        */
        bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }

+        /**
+           \brief Return Boolean expression to test whether expression is inf
+        */
+        expr mk_is_inf() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        /**
+           \brief Return Boolean expression to test for whether expression is a NaN
+        */
+        expr mk_is_nan() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        /**
+           \brief Convert this fpa into an IEEE BV
+        */
+        expr mk_to_ieee_bv() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
        /**
           \brief Return string representation of numeral or algebraic number
           This method assumes the expression is numeral or algebraic
@ -1271,6 +1308,21 @@ namespace z3 {
          */
        friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);

+        /**
+           \brief Create an expression of FloatingPoint sort from three bit-vector expressions
+        */
+        friend expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig);
+
+        /**
+           \brief Conversion of a floating-point term into a signed bit-vector.
+        */
+        friend expr fpa_to_sbv(expr const& t, unsigned sz);
+
+        /**
+           \brief Conversion of a floating-point term into an unsigned bit-vector.
+        */
+        friend expr fpa_to_ubv(expr const& t, unsigned sz);
+
        /**
           \brief sequence and regular expression operations.
           + is overloaded as sequence concatenation and regular expression union.
@ -1291,7 +1343,7 @@ namespace z3 {
            check_error();
            return expr(ctx(), r);
        }
-        expr contains(expr const& s) {
+        expr contains(expr const& s) const {
            check_context(*this, s);
            Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
            check_error();
@ -1768,6 +1820,27 @@ namespace z3 {
        return expr(a.ctx(), r);
    }

+    inline expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig) {
+        check_context(sgn, exp); check_context(exp, sig);
+        assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
+        Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
+        sgn.check_error();
+        return expr(sgn.ctx(), r);
+    }
+
+    inline expr fpa_to_sbv(expr const& t, unsigned sz) {
+        assert(t.is_fpa());
+        Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }
+
+    inline expr fpa_to_ubv(expr const& t, unsigned sz) {
+        assert(t.is_fpa());
+        Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }

    /**
       \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
@ -1818,6 +1891,18 @@ namespace z3 {
    inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
    inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
    inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
+    /**
+       \brief signed greater than or equal to operator for bitvectors.
+    */
+    inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }
+    inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); }
+    /**
+       \brief signed greater than operator for bitvectors.
+    */
+    inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }
+    inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); }


    /**
@ -1985,8 +2070,7 @@ namespace z3 {

    template<typename T>
    template<typename T2>
-    array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]) {
-        m_size  = v.size();
+    array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
        for (unsigned i = 0; i < m_size; i++) {
            m_array[i] = v[i];
        }
@ -2937,8 +3021,16 @@ namespace z3 {
            return *this;
        }
        operator Z3_fixedpoint() const { return m_fp; }
-        void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
-        void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
+        expr_vector from_string(char const* s) { 
+            Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s); 
+            check_error(); 
+            return expr_vector(ctx(), r);
+        }
+        expr_vector from_file(char const* s) { 
+            Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s); 
+            check_error(); 
+            return expr_vector(ctx(), r);
+        }
        void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
        void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
        check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
@ -3176,6 +3268,7 @@ namespace z3 {
    inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
    inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
    inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
+    inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
    inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
    inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }

--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@ -140,7 +140,7 @@ endforeach()
 # Note, nuget package file names do not have the ${VER_REV} part.

 set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+if(TARGET_ARCHITECTURE STREQUAL "i686")
    set(Z3_DOTNET_PLATFORM "x86")
 else()
    set(Z3_DOTNET_PLATFORM "AnyCPU")
--- a/src/api/dotnet/Microsoft.Z3.csproj.in
+++ b/src/api/dotnet/Microsoft.Z3.csproj.in
@ -83,6 +83,9 @@ ${Z3_DOTNET_COMPILE_ITEMS}
    <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so')">
      <PackagePath>runtimes\linux-x64\native</PackagePath>
    </Content>
+    <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dylib" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dylib')">
+      <PackagePath>runtimes\macos\native</PackagePath>
+    </Content>
  </ItemGroup>

  <!-- Native binaries for x86; currently only Windows is supported. -->
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@ -898,7 +898,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
            continue;
        }
        if (is_mul(term)) {
-            rational r(mul), n(0);
+            r = mul;
+            rational n(0);
            for (expr* arg : *to_app(term)) {
                if (!is_extended_numeral(arg, n))
                    return false;
@ -907,7 +908,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
            return true;
        }
        if (is_add(term)) {
-            rational r(0), n(0);
+            rational n(0);
+            r = 0;
            for (expr* arg : *to_app(term)) {
                if (!is_extended_numeral(arg, n))
                    return false;
@ -921,8 +923,7 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
        if (is_sub(term, t1, t2) && 
            is_extended_numeral(t1, k1) &&
            is_extended_numeral(t2, k2)) {
-            r = k1 - k2;
-            r *= mul;
+            r = (k1 - k2) * mul;
            return true;
        }
        return false;
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@ -718,7 +718,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
    op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
    op_names.push_back(builtin_name("bit2bool", OP_BIT2BOOL));

-    if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD") {
+    if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD" || logic == "HORN") {
        op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
        op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
        op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));
@ -827,6 +827,15 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
    return true;
 }

+bool bv_recognizers::is_repeat(expr const * e, expr*& arg, unsigned& n) const {
+    if (!is_app_of(e, get_fid(), OP_REPEAT))
+        return false;
+    arg = to_app(e)->get_arg(0);
+    n = to_app(e)->get_parameter(0).get_int();
+    return true;
+}
+
+
 bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
    if (!is_bv2int(e)) return false;
    r = to_app(e)->get_arg(0);
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@ -310,6 +310,7 @@ public:
    unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
    unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
    bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const;
+    bool is_repeat(expr const * e, expr*& arg, unsigned& n) const;
    bool is_bv2int(expr const * e, expr * & r) const;
    bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
    bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@ -281,21 +281,36 @@ namespace euf {
       VERIFY(n->num_args() == 0 || !n->merge_enabled() || m_table.contains(n));
    }

-    void egraph::set_value(enode* n, lbool value) {        
-        force_push();
-        TRACE("euf", tout << bpp(n) << "\n";);
-        SASSERT(n->value() == l_undef);
-        n->set_value(value);
-        m_updates.push_back(update_record(n, update_record::value_assignment()));
+    void egraph::set_value(enode* n, lbool value) {  
+        if (n->value() == l_undef) {
+            force_push();
+            TRACE("euf", tout << bpp(n) << " := " << value << "\n";);
+            n->set_value(value);
+            m_updates.push_back(update_record(n, update_record::value_assignment()));
+        }
    }

    void egraph::set_lbl_hash(enode* n) {
-        NOT_IMPLEMENTED_YET();
+        SASSERT(n->m_lbl_hash == -1);
+        // m_lbl_hash should be different from -1, if and only if,
+        // there is a pattern that contains the enode. So,
+        // I use a trail to restore the value of m_lbl_hash to -1.
+        m_updates.push_back(update_record(n, update_record::lbl_hash()));
+        unsigned h = hash_u(n->get_expr_id());
+        n->m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
+        // propagate modification to the root m_lbls set.
+        enode* r = n->get_root();
+        approx_set & r_lbls = r->m_lbls;
+        if (!r_lbls.may_contain(n->m_lbl_hash)) {
+            m_updates.push_back(update_record(r, update_record::lbl_set()));
+            r_lbls.insert(n->m_lbl_hash);
+        }
    }

    void egraph::pop(unsigned num_scopes) {
        if (num_scopes <= m_num_scopes) {
            m_num_scopes -= num_scopes;
+            m_to_merge.reset();
            return;
        }
        num_scopes -= m_num_scopes;
@ -355,6 +370,12 @@ namespace euf {
                VERIFY(p.r1->value() != l_undef);
                p.r1->set_value(l_undef);
                break;
+            case update_record::tag_t::is_lbl_hash:
+                p.r1->m_lbl_hash = p.m_lbl_hash;
+                break;
+            case update_record::tag_t::is_lbl_set:
+                p.r1->m_lbls.set(p.m_lbls);
+                break;
            default:
                UNREACHABLE();
                break;
@ -439,8 +460,8 @@ namespace euf {
                auto rc = insert_table(p);
                enode* p_other = rc.first;
                SASSERT(m_table.contains_ptr(p) == (p_other == p));
-                if (p_other != p)
-                    m_to_merge.push_back(to_merge(p_other, p, rc.second));
+                if (p_other != p) 
+                    m_to_merge.push_back(to_merge(p_other, p, rc.second));                
                else
                    r2->m_parents.push_back(p);
                if (p->is_equality())
@ -704,8 +725,6 @@ namespace euf {
                TRACE("euf", display(tout << bpp(n) << " is not closed under congruence\n"););
                UNREACHABLE();
            }
-
-
    }

    std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
@ -765,7 +784,6 @@ namespace euf {

    void egraph::copy_from(egraph const& src, std::function<void*(void*)>& copy_justification) {
        SASSERT(m_scopes.empty());
-        SASSERT(src.m_scopes.empty());
        SASSERT(m_nodes.empty());
        ptr_vector<enode> old_expr2new_enode, args;
        ast_translation tr(src.m, m);
@ -793,6 +811,9 @@ namespace euf {
                merge(n2, n2t, n1->m_justification.copy(copy_justification));
        }
        propagate();
+        for (unsigned i = 0; i < src.m_scopes.size(); ++i)
+            push();
+        force_push();
    }
 }

--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@ -102,9 +102,12 @@ namespace euf {
            struct new_lits_qhead {};
            struct inconsistent {};
            struct value_assignment {};
+            struct lbl_hash {};
+            struct lbl_set {};
            enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, 
-                         is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
-                         is_new_th_eq_qhead, is_new_lits_qhead, is_inconsistent, is_value_assignment };
+                    is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
+                    is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, 
+                    is_inconsistent, is_value_assignment, is_lbl_set };
            tag_t  tag;
            enode* r1;
            enode* n1;
@ -116,6 +119,8 @@ namespace euf {
                };
                unsigned qhead;
                bool     m_inconsistent;
+                signed char m_lbl_hash;
+                unsigned long long m_lbls;
            };
            update_record(enode* r1, enode* n1, unsigned r2_num_parents) :
                tag(tag_t::is_set_parent), r1(r1), n1(n1), r2_num_parents(r2_num_parents) {}
@ -139,6 +144,10 @@ namespace euf {
                tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {}
            update_record(enode* n, value_assignment) :
                tag(tag_t::is_value_assignment), r1(n), n1(nullptr), qhead(0) {}
+            update_record(enode* n, lbl_hash):
+                tag(tag_t::is_lbl_hash), r1(n), n1(nullptr), m_lbl_hash(n->m_lbl_hash) {}
+            update_record(enode* n, lbl_set):
+                tag(tag_t::is_lbl_set), r1(n), n1(nullptr), m_lbls(n->m_lbls.get()) {}    
        };
        ast_manager&           m;
        svector<to_merge>      m_to_merge;
--- a/src/ast/euf/euf_etable.cpp
+++ b/src/ast/euf/euf_etable.cpp
@ -72,7 +72,7 @@ namespace euf {
    void * etable::mk_table_for(unsigned arity, func_decl * d) {
        void * r;
        SASSERT(d->get_arity() >= 1);
-        SASSERT(arity >= d->get_arity());
+        SASSERT(arity >= d->get_arity() || d->is_associative());
        switch (arity) {
        case 1:
            r = TAG(void*, alloc(unary_table), UNARY);
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@ -336,8 +336,13 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
    //
    quantifier* lam = nullptr;
    for (unsigned i = 0; i < num_args; ++i) {
-        if (is_lambda(args[i])) {
+        if (is_lambda(args[i]))
            lam = to_quantifier(args[i]);
+        else if (m_util.is_const(args[i]))
+            continue;
+        else {
+            lam = nullptr;
+            break;
        }
    }
    if (lam) {
@ -351,15 +356,6 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
                lam = to_quantifier(a);
                args1.push_back(lam->get_expr());
            }
-            else {
-                expr_ref_vector sel(m());
-                sel.push_back(a);
-                unsigned n = lam->get_num_decls();
-                for (unsigned i = 0; i < n; ++i) {
-                    sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i)));
-                }
-                args1.push_back(m_util.mk_select(sel.size(), sel.data()));
-            }
        }
        result = m().mk_app(f, args1.size(), args1.data());
        result = m().update_quantifier(lam, result);
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@ -437,7 +437,7 @@ namespace seq {
        expr_ref t_eq_empty = mk_eq_empty(t);

        // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
-        // ~contains(t,s) <=> indexof(t,s,offset) = -1
+        // ~contains(t,s) => indexof(t,s,offset) = -1

        add_clause(cnt,  i_eq_m1);
        add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
@ -489,7 +489,7 @@ namespace seq {
            // 0 <= offset & offset < len(t) => len(x) = offset
            // 0 <= offset & offset < len(t) & indexof(y,s,0) = -1 => -1 = i
            // 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 =>
-            //                  -1 = indexof(y,s,0) + offset = indexof(t, s, offset)
+            //                  indexof(y,s,0) + offset = indexof(t, s, offset)

            add_clause(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
            add_clause(~offset_ge_0, offset_ge_len, mk_eq(mk_len(x), offset));
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@ -1492,6 +1492,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
 seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) const {
    if (is_known()) {
        unsigned m = min_length * lower;
+        // Code review: this is not a complete overflow check. 
        if (m > 0 && (m < min_length || m < lower))
            m = UINT_MAX;
        lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@ -104,7 +104,7 @@ void static_features::reset() {
    m_num_aliens_per_family                .reset();
    m_num_theories                         = 0;
    m_theories                             .reset();
-    m_max_stack_depth                      = 500;
+    m_max_stack_depth                      = 100;
    flush_cache();
 }

@ -404,10 +404,11 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
        m_num_sharing++;
        return;
    }    
+
    if (stack_depth > m_max_stack_depth) {
        for (expr* arg : subterms(expr_ref(e, m)))
            if (get_depth(arg) <= 3 || is_quantifier(arg)) 
-                process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth-10);
+                process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10);
        return;
    }
    mark(e);
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@ -877,10 +877,11 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
 }

 void cmd_context::insert(symbol const & s, psort_decl * p) {
+    pm().inc_ref(p);
    if (m_psort_decls.contains(s)) {
+        pm().dec_ref(p);
        throw cmd_exception("sort already defined ", s);
    }
-    pm().inc_ref(p);
    m_psort_decls.insert(s, p);
    if (!m_global_decls) {
        m_psort_decls_stack.push_back(s);
@ -1122,7 +1123,7 @@ bool cmd_context::try_mk_builtin_app(symbol const & s, unsigned num_args, expr *
        result = m().mk_app(fid, k, num_indices, indices, num_args, args, range);
    }
    CHECK_SORT(result.get());
-    return true;
+    return nullptr != result.get();
 }

 bool cmd_context::try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args, 
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@ -1246,8 +1246,8 @@ namespace dd {
            }
            else {
                set_mark(r);
-                m_todo.pop_back();
-                m_todo.push_back(lo(r)).push_back(hi(r));
+                m_todo.push_back(lo(r));
+                m_todo.push_back(hi(r));
            }
        }
        return max_d;
--- a/src/math/hilbert/hilbert_basis.h
+++ b/src/math/hilbert/hilbert_basis.h
@ -89,7 +89,7 @@ class hilbert_basis {
    reslimit&          m_limit;
    vector<num_vector> m_ineqs;      // set of asserted inequalities
    bool_vector      m_iseq;       // inequalities that are equalities
-    num_vector         m_store;      // store of vectors
+    mutable num_vector         m_store;      // store of vectors
    svector<offset_t>  m_basis;      // vector of current basis
    svector<offset_t>  m_free_list;  // free list of unused storage
    svector<offset_t>  m_active;     // active set
--- a/src/math/lp/factorization.cpp
+++ b/src/math/lp/factorization.cpp
@ -23,21 +23,30 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
    std::sort(k_vars.begin(), k_vars.end());
    std::sort(j_vars.begin(), j_vars.end());

+    if (false && m_num_failures > 10) {
+        for (bool& m : m_mask) m = true;
+        m_mask[0] = false;
+        m_full_factorization_returned = true;
+        return false;
+    }
    if (k_vars.size() == 1) {
        k.set(k_vars[0], factor_type::VAR);
    } else {
        unsigned i;
        if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) {
+            ++m_num_failures;
            return false;
        }
        k.set(i, factor_type::MON);
    }
+    m_num_failures = 0;

    if (j_vars.size() == 1) {
        j.set(j_vars[0], factor_type::VAR);
    } else {
        unsigned i;
        if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) {
+            ++m_num_failures;
            return false;
        }
        j.set(i, factor_type::MON);
@ -46,7 +55,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
 }

 factorization const_iterator_mon::operator*() const {
-    if (m_full_factorization_returned == false)  {
+    if (!m_full_factorization_returned)  {
        return create_full_factorization(m_ff->m_monic);
    }
    factor j, k; rational sign;
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@ -30,12 +30,12 @@ struct factorization_factory;
 enum class factor_type { VAR, MON };

 class factor {
-    lpvar        m_var;
-    factor_type  m_type;
-    bool        m_sign;
+    lpvar        m_var{ UINT_MAX };
+    factor_type  m_type{ factor_type::VAR };
+    bool         m_sign{ false };
 public:
    factor(): factor(false) {}
-    factor(bool sign): m_var(UINT_MAX), m_type(factor_type::VAR), m_sign(sign) {}
+    factor(bool sign): m_sign(sign) {}
    explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
    unsigned var() const { return m_var; }
    factor_type type() const { return m_type; }
@ -77,9 +77,10 @@ public:

 struct const_iterator_mon {
    // fields
-    bool_vector                  m_mask;
+    mutable bool_vector                    m_mask;
    const factorization_factory *  m_ff;
-    bool                           m_full_factorization_returned;
+    mutable bool                           m_full_factorization_returned;
+    mutable unsigned               m_num_failures{ 0 };

    // typedefs
    typedef const_iterator_mon self_type;
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@ -61,7 +61,7 @@ namespace lp {
            return true;
        const lar_term* t = lra.terms()[i];
        impq delta = get_cube_delta_for_term(*t);
-        TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta;);
+        TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta << "\n";);
        if (is_zero(delta))
            return true;
        return lra.tighten_term_bounds_by_delta(tv::term(i), delta);
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@ -2331,15 +2331,16 @@ namespace lp {
                v = flv;
            }
            m_incorrect_columns.insert(j);
-            TRACE("cube", tout << "new val = " << v << "\n";);
+            TRACE("cube", tout << "new val = " << v << " column: " << j << "\n";);
        }
-        if (m_incorrect_columns.size()) {
+        if (!m_incorrect_columns.empty()) {
            fix_terms_with_rounded_columns();
            m_incorrect_columns.clear();
        }
    }

    void lar_solver::fix_terms_with_rounded_columns() {
+
        for (unsigned i = 0; i < m_terms.size(); i++) {
            if (!term_is_used_as_row(i))
                continue;
@ -2357,8 +2358,10 @@ namespace lp {
                m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
            }
        }
+
        SASSERT(ax_is_correct());
    }
+
    // return true if all y coords are zeroes
    bool lar_solver::sum_first_coords(const lar_term& t, mpq& val) const {
        val = zero_of_type<mpq>();
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@ -66,7 +66,7 @@ namespace lp_api {
        lp::constraint_index get_constraint(bool b) const { return m_constraints[b]; }

        inf_rational get_value(bool is_true) const {
-            if (is_true) 
+            if (is_true != get_lit().sign()) 
                return inf_rational(m_value);                         // v >= value or v <= value
            if (m_is_int) {
                SASSERT(m_value.is_int());
--- a/src/math/polynomial/linear_eq_solver.h
+++ b/src/math/polynomial/linear_eq_solver.h
@ -34,7 +34,7 @@ public:
    
    void flush() {
        SASSERT(b.size() == A.size());
-        unsigned sz = A.size();
+        auto sz = A.size();
        for (unsigned i = 0; i < sz; i++) {
            svector<numeral> & as = A[i];
            m.del(b[i]);
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@ -4096,7 +4096,7 @@ namespace polynomial {
        // select a new random value in GF(p) that is not in vals, and store it in r
        void peek_fresh(scoped_numeral_vector const & vals, unsigned p, scoped_numeral & r) {
            SASSERT(vals.size() < p); // otherwise we can't keep the fresh value
-            unsigned sz = vals.size();
+            auto sz = vals.size();
            while (true) {
                m().set(r, rand() % p);
                // check if fresh value...
@ -6240,7 +6240,7 @@ namespace polynomial {
            }

            void reset() {
-                unsigned sz = m_xs.size();
+                auto sz = m_xs.size();
                for (unsigned i = 0; i < sz; i++) {
                    m_max_degree[m_xs[i]] = 0;
                }
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@ -2126,7 +2126,7 @@ namespace upolynomial {
        }
        frame_stack.push_back(drs_frame(parent_idx, sz, true));
        // right child
-        translate(sz, p_stack.end() - sz, p_aux);
+        translate(sz, p_stack.data() + p_stack.size() - sz, p_aux);
        normalize(p_aux);
        for (unsigned i = 0; i < sz; i++) {
            p_stack.push_back(numeral());
@ -2226,7 +2226,7 @@ namespace upolynomial {
            drs_frame & fr    = frame_stack.back();
            unsigned sz       = fr.m_size;
            SASSERT(sz <= p_stack.size());
-            numeral const * p = p_stack.end() - sz;
+            numeral const * p = p_stack.data() + p_stack.size() - sz;
            TRACE("upolynomial", tout << "processing frame #" << frame_stack.size() - 1 << "\n"
                  << "first: " << fr.m_first << ", left: " << fr.m_left << ", sz: " << fr.m_size << ", parent_idx: ";
                  if (fr.m_parent_idx == UINT_MAX) tout << "<null>"; else tout << fr.m_parent_idx;
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@ -39,8 +39,9 @@ namespace opt {
    class model_based_opt {
    public:
        struct var {
-            unsigned m_id;
+            unsigned m_id { 0 };
            rational m_coeff;
+            var() {}
            var(unsigned id, rational const& c): m_id(id), m_coeff(c) {}
            struct compare {
                bool operator()(var x, var y) {
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@ -616,7 +616,6 @@ struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
                                    false, // no proofs for evaluator
                                    m_cfg),
        m_cfg(md.get_manager(), md, p) {
-        set_cancel_check(false);
    }
    void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
    void reset() {
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@ -202,12 +202,14 @@ namespace opt {
        return r;
    }

-    void opt_solver::maximize_objectives(expr_ref_vector& blockers) {
+    bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
        expr_ref blocker(m);
        for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
-            maximize_objective(i, blocker);
+            if (!maximize_objective(i, blocker))
+                return false;
            blockers.push_back(blocker);
        }
+        return true;
    }

    lbool opt_solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
@ -238,7 +240,7 @@ namespace opt {
       Precondition: the state of the solver is satisfiable and such that a current model can be extracted.
       
    */
-    void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
+    bool opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
        smt::theory_var v = m_objective_vars[i];
        bool has_shared = false;
        m_last_model = nullptr;
@ -256,8 +258,9 @@ namespace opt {
            SASSERT(has_shared);
            decrement_value(i, val);
            if (l_true != m_context.check(0, nullptr))  
-                throw default_exception("maximization suspended");
-            m_context.get_model(m_last_model);            
+                return false;
+            m_context.get_model(m_last_model);      
+            return true;
        };

        if (!val.is_finite()) {
@ -268,15 +271,15 @@ namespace opt {
            m_last_model = nullptr;
            m_context.get_model(m_last_model);
            if (has_shared && val != current_objective_value(i)) {
-                decrement();
+                if (!decrement())
+                    return false;
            }
            else {
                m_models.set(i, m_last_model.get());
            }
        }
-        else {
-            decrement();
-        }
+        else if (!decrement())
+            return false;
        m_objective_values[i] = val;
        TRACE("opt", { 
                tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
@ -285,6 +288,7 @@ namespace opt {
                if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); 
                if (m_last_model) model_smt2_pp(tout << "last model:\n", m, *m_last_model, 0);
            });
+        return true;
    }

    lbool opt_solver::decrement_value(unsigned i, inf_eps& val) {
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@ -119,8 +119,8 @@ namespace opt {

        smt::theory_var add_objective(app* term);
        void reset_objectives();
-        void maximize_objective(unsigned i, expr_ref& blocker);
-        void maximize_objectives(expr_ref_vector& blockers);
+        bool maximize_objective(unsigned i, expr_ref& blocker);
+        bool maximize_objectives1(expr_ref_vector& blockers);
        inf_eps const & saved_objective_value(unsigned obj_index);
        inf_eps current_objective_value(unsigned obj_index);
        model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@ -321,7 +321,8 @@ namespace opt {
                is_sat = m_s->check_sat(1,vars);
                if (is_sat == l_true) {
                    disj.reset();
-                    m_s->maximize_objectives(disj);
+                    if (!m_s->maximize_objectives1(disj)) 
+                        return l_undef;
                    m_s->get_model(m_model);       
                    m_s->get_labels(m_labels);            
                    for (unsigned i = 0; i < ors.size(); ++i) {
@ -395,7 +396,8 @@ namespace opt {
        expr_ref_vector disj(m);
        m_s->get_model(m_model);
        m_s->get_labels(m_labels);
-        m_s->maximize_objectives(disj);
+        if (!m_s->maximize_objectives1(disj))
+            return expr_ref(m.mk_true(), m);
        set_max(m_lower, m_s->get_objective_values(), disj);
        TRACE("opt", model_pp(tout << m_lower << "\n", *m_model););
        IF_VERBOSE(2, verbose_stream() << "(optsmt.lower " << m_lower << ")\n";);
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@ -1944,6 +1944,8 @@ namespace smt2 {
                expr ** expr_it   = expr_stack().data() + fr->m_expr_spos;
                expr ** expr_end  = expr_it + num_decls;
                for (; expr_it != expr_end; ++expr_it, ++sym_it) {
+                    if (!(*expr_it))
+                        throw parser_exception("invalid let expression");
                    TRACE("let_frame", tout << "declaring: " << *sym_it << " " << mk_pp(*expr_it, m()) << "\n";);
                    m_env.insert(*sym_it, local(*expr_it, m_num_bindings));
                }
@ -2569,7 +2571,7 @@ namespace smt2 {
                throw cmd_exception("invalid assert command, expression required as argument");
            }
            expr * f = expr_stack().back();
-            if (!m().is_bool(f)) {
+            if (!f || !m().is_bool(f)) {
                TRACE("smt2parser", tout << expr_ref(f, m()) << "\n";);
                throw cmd_exception("invalid assert command, term is not Boolean");
            }
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@ -68,7 +68,7 @@ namespace sat {
        symbol m_name;
        solver* m_solver { nullptr };
    public:        
-        extension(symbol const& name, int id): m_id(id), m_name(name) {}
+        extension(symbol const& name, int id): m_id(id), m_name(name) { }
        virtual ~extension() {}
        int get_id() const { return m_id; }
        void set_solver(solver* s) { m_solver = s; }        
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@ -1296,7 +1296,7 @@ namespace sat {
            return do_local_search(num_lits, lits);
        }
        if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || 
-             m_config.m_ddfw_threads > 0) && !m_par) {
+             m_config.m_ddfw_threads > 0) && !m_par && !m_ext) {
            SASSERT(scope_lvl() == 0);
            return check_par(num_lits, lits);
        }
@ -1440,6 +1440,9 @@ namespace sat {
        if (!rlimit().inc()) {
            return l_undef;
        }
+        if (m_ext)
+            return l_undef;
+
        scoped_ptr_vector<i_local_search> ls;
        scoped_ptr_vector<solver> uw;
        int num_extra_solvers = m_config.m_num_threads - 1;
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@ -164,7 +164,7 @@ namespace arith {
        unsigned index = 0;
        while (index < terms.size()) {
            SASSERT(index >= vars.size());
-            expr* n = terms[index].get();
+            expr* n = terms.get(index);
            st.to_ensure_enode().push_back(n);
            if (a.is_add(n)) {
                for (expr* arg : *to_app(n)) {
@ -382,7 +382,7 @@ namespace arith {
        updt_unassigned_bounds(v, +1);
        m_bounds_trail.push_back(v);
        m_bool_var2bound.insert(bv, b);
-        TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
+        TRACE("arith_verbose", tout << "Internalized " << lit << ": " << mk_pp(atom, m) << " " << *b << "\n";);
        m_new_bounds.push_back(b);
        //add_use_lists(b);
        return true;
@ -391,7 +391,7 @@ namespace arith {

    bool solver::internalize_term(expr* term) {
        if (!has_var(term))
-            internalize_def(term);
+            register_theory_var_in_lar_solver(internalize_def(term));
        return true;
    }

@ -583,11 +583,10 @@ namespace arith {
        if (e->is_attached_to(get_id()))
            return e->get_th_var(get_id());
        theory_var v = mk_var(e);
-        TRACE("arith", tout << "fresh var: v" << v << " " << mk_pp(n, m) << "\n";);
+        TRACE("arith_verbose", tout << "v" << v << " " << mk_pp(n, m) << "\n";);
        SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
        reserve_bounds(v);
        ctx.attach_th_var(e, this, v);
-        TRACE("arith", tout << mk_pp(n, m) << " " << v << "\n";);
        SASSERT(euf::null_theory_var != v);
        return v;
    }
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@ -145,7 +145,7 @@ namespace arith {
        bool v_is_int = b.is_int();
        literal lit2 = sat::null_literal;
        bool find_glb = (is_true == (k == lp_api::lower_t));
-        TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
+        TRACE("arith", tout << lit1 << " v" << v << " val " << val << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
        if (find_glb) {
            rational glb;
            api_bound* lb = nullptr;
@ -187,6 +187,7 @@ namespace arith {
        m_params.push_back(parameter(m_farkas));
        m_params.push_back(parameter(rational(1)));
        m_params.push_back(parameter(rational(1)));
+        TRACE("arith", tout << lit2 << " <- " << m_core << "\n";);
        assign(lit2, m_core, m_eqs, m_params);
        ++m_stats.m_bounds_propagations;
    }
@ -1001,6 +1002,8 @@ namespace arith {
            ++m_stats.m_assume_eqs;
            return sat::check_result::CR_CONTINUE;
        }
+        if (!check_delayed_eqs()) 
+            return sat::check_result::CR_CONTINUE;
        if (m_not_handled != nullptr) {
            TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
            return sat::check_result::CR_GIVEUP;
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@ -39,8 +39,10 @@ namespace array {
                dep.add(n, p->get_arg(i));
        }
        for (euf::enode* k : euf::enode_class(n)) 
-            if (a.is_const(k->get_expr()))
-                dep.add(n, k->get_arg(0));    
+            if (a.is_const(k->get_expr())) 
+                dep.add(n, k->get_arg(0)); 
+        if (!dep.deps().contains(n))
+            dep.insert(n, nullptr);
        return true;
    }

--- a/src/sat/smt/bv_ackerman.cpp
+++ b/src/sat/smt/bv_ackerman.cpp
@ -31,6 +31,8 @@ namespace bv {
    }

    void ackerman::reset() {
+        while (m_queue)
+            remove(m_queue->prev());     
        m_table.reset();
        m_queue = nullptr;        
    }
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@ -90,7 +90,7 @@ namespace bv {
        m_wpos.push_back(0);
        m_zero_one_bits.push_back(zero_one_bits());       
        ctx.attach_th_var(n, this, r);        
-        TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_bounded_pp(n->get_expr(), m) << "\n";);
+        TRACE("bv", tout << "mk-var: v" << r << " " << n->get_expr_id() << " " << mk_bounded_pp(n->get_expr(), m) << "\n";);
        return r;
    }

@ -157,11 +157,15 @@ namespace bv {
        std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref& bit)> ebin;
        std::function<void(unsigned sz, expr* const* xs, expr_ref_vector& bits)> un;
        std::function<void(unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits)> pun;
+        std::function<expr*(expr* x, expr* y)> ibin;
+        std::function<expr*(expr* x)> iun;
+
 #define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
 #define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un);
 #define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
+#define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);

        switch (a->get_decl_kind()) {
        case OP_BV_NUM:           internalize_num(a); break;
@ -209,10 +213,15 @@ namespace bv {
        case OP_BSUB:             internalize_sub(a); break;
        case OP_CONCAT:           internalize_concat(a); break;
        case OP_EXTRACT:          internalize_extract(a); break;
+        case OP_REPEAT:           internalize_repeat(a); break;
        case OP_MKBV:             internalize_mkbv(a); break;
        case OP_INT2BV:           internalize_int2bv(a); break;
        case OP_BV2INT:           internalize_bv2int(a); break;
-        case OP_BUDIV:            internalize_udiv(a); break;
+        case OP_BUDIV:            internalize_int(bv.mk_bv_udiv_i, bv.mk_bv_udiv0); break;
+        case OP_BSDIV:            internalize_int(bv.mk_bv_sdiv_i, bv.mk_bv_sdiv0); break;
+        case OP_BSREM:            internalize_int(bv.mk_bv_srem_i, bv.mk_bv_srem0); break;
+        case OP_BUREM:            internalize_int(bv.mk_bv_urem_i, bv.mk_bv_urem0); break;
+        case OP_BSMOD:            internalize_int(bv.mk_bv_smod_i, bv.mk_bv_smod0); break;
        case OP_BSDIV0:           break;
        case OP_BUDIV0:           break;
        case OP_BSREM0:           break;
@ -280,6 +289,7 @@ namespace bv {
        SASSERT(l == mk_true() || ~l == mk_true());
        bool is_true = l == mk_true();
        zero_one_bits& bits = m_zero_one_bits[v];
+        TRACE("bv", tout << "register v" << v << " " << l << " " << mk_true() << "\n";);
        bits.push_back(zero_one_bit(v, idx, is_true));
    }

@ -516,19 +526,20 @@ namespace bv {
        internalize_binary(a, bin);
    }

-    void solver::internalize_udiv(app* n) {
+    void solver::internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& iun) {
        bv_rewriter_params p(s().params());
        expr* arg1 = n->get_arg(0);
        expr* arg2 = n->get_arg(1);
+        mk_bits(get_th_var(n));
        if (p.hi_div0()) {
-            add_unit(eq_internalize(n, bv.mk_bv_udiv_i(arg1, arg2)));
+            add_unit(eq_internalize(n, ibin(arg1, arg2)));
            return;
        }
        unsigned sz = bv.get_bv_size(n);
        expr_ref zero(bv.mk_numeral(0, sz), m);
        expr_ref eq(m.mk_eq(arg2, zero), m);
-        expr_ref udiv(m.mk_ite(eq, bv.mk_bv_udiv0(arg1), bv.mk_bv_udiv_i(arg1, arg2)), m);
-        add_unit(eq_internalize(n, udiv));
+        expr_ref ite(m.mk_ite(eq, iun(arg1), ibin(arg1, arg2)), m);
+        add_unit(eq_internalize(n, ite));
    }

    void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
@ -559,7 +570,7 @@ namespace bv {
    }

    void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
-        SASSERT(e->get_num_args() >= 2);
+        SASSERT(e->get_num_args() >= 1);
        expr_ref_vector bits(m), new_bits(m), arg_bits(m);
        unsigned i = e->get_num_args() - 1;
        get_arg_bits(e, i, bits);
@ -632,6 +643,18 @@ namespace bv {
        find_wpos(v);
    }

+    void solver::internalize_repeat(app* e) {
+        unsigned n = 0;
+        expr* arg = nullptr;
+        VERIFY(bv.is_repeat(e, arg, n));
+        expr_ref_vector conc(m);
+        for (unsigned i = 0; i < n; ++i)
+            conc.push_back(arg);
+        expr_ref r(bv.mk_concat(conc), m);
+        mk_bits(get_th_var(e));
+        add_unit(eq_internalize(e, r));
+    }
+
    void solver::internalize_bit2bool(app* n) {
        unsigned idx = 0;
        expr* arg = nullptr;
--- a/src/sat/smt/bv_invariant.cpp
+++ b/src/sat/smt/bv_invariant.cpp
@ -93,8 +93,16 @@ namespace bv {
        } while (curr != v);

        zero_one_bits const& _bits = m_zero_one_bits[v];
-        if (_bits.size() != num_bits)
-            std::cout << v << " " << _bits.size() << " " << num_bits << "\n";
+        if (_bits.size() != num_bits) {
+            std::cout << "v" << v << " " << _bits.size() << " " << num_bits << "\n";
+            std::cout << "true: " << mk_true() << "\n";
+            do {
+                std::cout << "v" << curr << ": " << m_bits[curr] << "\n";
+                curr = m_find.next(curr);
+            }
+            while (curr != v);
+        }
+        SASSERT(_bits.size() == num_bits);
        VERIFY(_bits.size() == num_bits);
        bool_vector already_found;
        already_found.resize(bv_sz, false);
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@ -661,9 +661,10 @@ namespace bv {
            result->m_bits[i].append(m_bits[i]);
            result->m_zero_one_bits[i].append(m_zero_one_bits[i]);
        }
+        result->set_solver(&ctx.s());
        for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
            if (find(i) != i)
-                result->m_find.merge(i, find(i));
+                result->m_find.set_root(i, find(i));
        result->m_prop_queue.append(m_prop_queue);
        for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) {
            atom* a = m_bool_var2atom[i];
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@ -102,6 +102,9 @@ namespace bv {
            unsigned   m_is_true:1;
            zero_one_bit(theory_var v = euf::null_theory_var, unsigned idx = UINT_MAX, bool is_true = false):
                m_owner(v), m_idx(idx), m_is_true(is_true) {}
+            std::ostream& display(std::ostream& out) const {
+                return out << "v" << m_owner << " @ " << m_idx << " " << (m_is_true?"T":"F");
+            }
        };

        typedef svector<zero_one_bit> zero_one_bits;
@ -239,6 +242,7 @@ namespace bv {
        void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
        void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
        void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
+        void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
        void internalize_num(app * n);       
        void internalize_concat(app * n);        
        void internalize_bv2int(app* n);
@ -248,8 +252,8 @@ namespace bv {
        void internalize_carry(app* n);
        void internalize_sub(app* n);
        void internalize_extract(app* n);
+        void internalize_repeat(app* n);
        void internalize_bit2bool(app* n);
-        void internalize_udiv(app* n);
        void internalize_udiv_i(app* n);
        template<bool Signed, bool Reverse, bool Negated>
        void internalize_le(app* n);
@ -366,9 +370,12 @@ namespace bv {
        typedef std::pair<solver const*, theory_var> pp_var;
        pp_var pp(theory_var v) const { return pp_var(this, v); }

+        friend std::ostream& operator<<(std::ostream& out, solver::zero_one_bit const& zo) { return zo.display(out); }
+
    };

    inline std::ostream& operator<<(std::ostream& out, solver::pp_var const& p) { return p.first->display(out, p.second); }


+
 }
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@ -63,6 +63,7 @@ namespace dt {
        SASSERT(s.m_to_unmark2.empty());
        s.m_used_eqs.reset();
        s.m_dfs.reset();
+        s.m_parent.reset();
    }

    solver::final_check_st::~final_check_st() {
@ -692,6 +693,10 @@ namespace dt {

    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var) {
+            values.set(n->get_root_id(), mdl.get_fresh_value(n->get_sort()));
+            return;
+        }
        v = m_find.find(v);
        SASSERT(v != euf::null_theory_var);
        enode* con = m_var_data[v]->m_constructor;
@ -703,9 +708,11 @@ namespace dt {
    }

    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
-        theory_var v = n->get_th_var(get_id());
        if (!is_datatype(n->get_expr()))
-            return true;
+            return false;
+        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var) 
+            return false;
        euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
        if (con->num_args() == 0)
            dep.insert(n, nullptr);
@ -715,10 +722,8 @@ namespace dt {
    }

    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        if (!visit_rec(m, e, sign, root, redundant)) {
-            TRACE("dt", tout << mk_pp(e, m) << "\n";);
-            return sat::null_literal;
-        }
+        if (!visit_rec(m, e, sign, root, redundant)) 
+            return sat::null_literal;        
        auto lit = ctx.expr2literal(e);
        if (sign)
            lit.neg();
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@ -141,8 +141,7 @@ namespace euf {
        }

        m_bool_var2expr.reserve(v + 1, nullptr);
-        if (m_bool_var2expr[v]) {
-            SASSERT(m_egraph.find(e));
+        if (m_bool_var2expr[v] && m_egraph.find(e)) {
            SASSERT(m_egraph.find(e)->bool_var() == v);
            return lit;
        }
@ -158,6 +157,8 @@ namespace euf {
            m_egraph.set_merge_enabled(n, false);
        if (!si.is_bool_op(e))
            track_relevancy(lit.var());
+        if (s().value(lit) != l_undef) 
+            m_egraph.set_value(n, s().value(lit));
        return lit;
    }

--- a/src/sat/smt/euf_invariant.cpp
+++ b/src/sat/smt/euf_invariant.cpp
@ -48,8 +48,10 @@ namespace euf {
        if (s().inconsistent())
            return;
        for (enode* n : m_egraph.nodes())
-            if (m.is_false(n->get_root()->get_expr()) && m.is_eq(n->get_expr()) &&
-                n->get_arg(0)->get_root() == n->get_arg(1)->get_root()) {
+            if (m.is_false(n->get_root()->get_expr()) && 
+                m.is_eq(n->get_expr()) &&
+                !m.is_bool(n->get_app()->get_arg(0)) && 
+                (n->get_arg(0)->get_root() == n->get_arg(1)->get_root())) {
                enable_trace("euf");
                TRACE("euf", display(tout << n->get_expr_id() << ": " << mk_pp(n->get_expr(), m) << "\n" 
                                     << "#" << n->get_arg(0)->get_expr_id() << " == #" << n->get_arg(1)->get_expr_id() << " r: " << n->get_arg(0)->get_root_id() << "\n");
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@ -144,6 +144,16 @@ namespace euf {
                    m_values.set(id, m.mk_false());
                    continue;
                }
+                switch (n->value()) {
+                case l_true:
+                    m_values.set(id, m.mk_true());
+                    continue;
+                case l_false:
+                    m_values.set(id, m.mk_false());
+                    continue;
+                default:
+                    break;
+                }
                if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
                    continue;
                sat::bool_var v = get_enode(e)->bool_var();
@ -198,6 +208,7 @@ namespace euf {
                    fi = alloc(func_interp, m, arity);
                    mdl->register_decl(f, fi);
                }
+                TRACE("euf", tout << f->get_name() << "\n";);
                args.reset();                
                for (enode* arg : enode_args(n)) 
                    args.push_back(m_values.get(arg->get_root_id()));                
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@ -410,10 +410,8 @@ namespace q {
        mam::ground_subterms(pat, m_ground);
        for (expr* g : m_ground) { 
            euf::enode* n = ctx.get_egraph().find(g);
-            if (!n->is_attached_to(m_qs.get_id())) {
-                euf::theory_var v = m_qs.mk_var(n);
-                ctx.get_egraph().add_th_var(n, v, m_qs.get_id());
-            }
+            if (!n->is_attached_to(m_qs.get_id())) 
+                m_qs.mk_var(n);            
        }
    }

--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@ -96,7 +96,6 @@ namespace q {
    }

    euf::theory_var solver::mk_var(euf::enode* n) {
-        SASSERT(is_forall(n->get_expr()) || is_exists(n->get_expr()));
        auto v = euf::th_euf_solver::mk_var(n);
        ctx.attach_th_var(n, this, v);        
        return v;
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@ -162,13 +162,13 @@ namespace smt {
       The variables are replaced by skolem constants. These constants are stored in sks.
    */

-    void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
+    bool model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
        expr_ref tmp(m);
        
        TRACE("model_checker", tout << "curr_model:\n"; model_pp(tout, *m_curr_model););

        if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
-            return;
+            return false;
        }
        TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
        ptr_buffer<expr> subst_args;
@ -191,6 +191,7 @@ namespace smt {
        r = m.mk_not(sk_body);
        TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
        m_aux_context->assert_expr(r);
+        return true;
    }

    bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
@ -333,7 +334,8 @@ namespace smt {
        TRACE("model_checker", tout << "model checking:\n" << expr_ref(flat_q->get_expr(), m) << "\n";);
        expr_ref_vector sks(m);

-        assert_neg_q_m(flat_q, sks);
+        if (!assert_neg_q_m(flat_q, sks))
+            return false;
        TRACE("model_checker", tout << "skolems:\n" << sks << "\n";);

        flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@ -62,7 +62,7 @@ namespace smt {
        expr * get_type_compatible_term(expr * val);
        expr_ref replace_value_from_ctx(expr * e);
        void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
-        void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
+        bool assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
        bool add_blocking_clause(model * cex, expr_ref_vector & sks);
        bool check(quantifier * q);
        void check_quantifiers(bool& found_relevant, unsigned& num_failures);
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@ -74,7 +74,6 @@ namespace smt {
                for (auto const& kv : m_elems) {
                    m.dec_ref(kv.m_key);
                }
-                m_elems.reset();
            }

            obj_map<expr, unsigned> const& get_elems() const { return m_elems; }
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@ -1872,11 +1872,14 @@ public:

 app* theory_seq::get_ite_value(expr* e) {
    expr* e1, *e2, *e3;
-    while (m.is_ite(e, e1, e2, e3)) {
-        if (get_root(e2) == get_root(e)) {
+    while (m.is_ite(e, e1, e2, e3)) {        
+        if (!ctx.e_internalized(e))
+            break;
+        enode* r = ctx.get_enode(e)->get_root();
+        if (ctx.get_enode(e2)->get_root() == r) {
            e = e2;
        }
-        else if (get_root(e3) == get_root(e)) {
+        else if (ctx.get_enode(e3)->get_root() == r) {
            e = e3;
        }
        else {
--- a/src/util/approx_set.h
+++ b/src/util/approx_set.h
@ -70,6 +70,10 @@ public:
        m_set(s.m_set) {
    }

+    void set(R s) { m_set = s; }
+
+    R get() const { return m_set; }
+
    void insert(T const & e) {
        m_set |= e2s(e);
    }
@ -162,7 +166,7 @@ class approx_set : public u_approx_set {
 public:
    approx_set():u_approx_set() {}
    approx_set(unsigned e):u_approx_set(e) {}
-
+    
    class iterator {
        unsigned long long m_set;
        unsigned           m_val;
--- a/src/util/heap.h
+++ b/src/util/heap.h
@ -139,7 +139,7 @@ public:
        if (empty()) {
            return;
        }
-        memset(m_value2indices.begin(), 0, sizeof(int) * m_value2indices.size());
+        memset(m_value2indices.data(), 0, sizeof(int) * m_value2indices.size());
        m_values.reset();
        m_values.push_back(-1);
        CASSERT("heap", check_invariant());
@ -244,11 +244,11 @@ public:
    }

    iterator begin() { 
-        return m_values.begin() + 1; 
+        return m_values.data() + 1; 
    }

    iterator end() { 
-        return m_values.end(); 
+        return m_values.data() + m_values.size(); 
    }

    const_iterator begin() const { 
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@ -112,7 +112,7 @@ class mpff_manager {
    
    unsigned          m_precision;      //!< Number of words in the significand. Must be an even number.
    unsigned          m_precision_bits; //!< Number of bits in the significand.  Must be 32*m_precision.
-    unsigned_vector   m_significands;   //!< Array containing all significands.
+    mutable unsigned_vector   m_significands;   //!< Array containing all significands.
    unsigned          m_capacity;       //!< Number of significands that can be stored in m_significands.
    bool              m_to_plus_inf;    //!< If True, then round to plus infinity, otherwise to minus infinity
    id_gen            m_id_gen;
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@ -258,7 +258,7 @@ void mpfx_manager::set_core(mpfx & n, mpz_manager<SYNCH> & m, mpz const & v) {
        m_tmp_digits.reset();
        allocate_if_needed(n);
        n.m_sign = m.decompose(v, m_tmp_digits);
-        unsigned sz = m_tmp_digits.size();
+        auto sz = m_tmp_digits.size();
        if (sz > m_int_part_sz)
            throw overflow_exception();
        unsigned * w = words(n);
@ -299,7 +299,7 @@ void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
        }
        m_tmp_digits.reset();
        m.decompose(tmp, m_tmp_digits);
-        unsigned sz = m_tmp_digits.size();
+        auto sz = m_tmp_digits.size();
        if (sz > m_total_sz)
            throw overflow_exception();
        unsigned * w = words(n);
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@ -81,11 +81,11 @@ class mpfx_manager {
    unsigned          m_int_part_sz;
    unsigned          m_frac_part_sz;
    unsigned          m_total_sz;       //!< == m_int_part_sz + m_frac_part_sz
-    unsigned_vector   m_words;          //!< Array containing all words
+    mutable unsigned_vector   m_words;          //!< Array containing all words
    unsigned          m_capacity;       //!< Number of mpfx numerals that can be stored in m_words.
    bool              m_to_plus_inf;    //!< If True, then round to plus infinity, otherwise to minus infinity
    id_gen            m_id_gen;
-    unsigned_vector   m_buffer0, m_buffer1, m_buffer2;
+    mutable unsigned_vector   m_buffer0, m_buffer1, m_buffer2;
    unsigned_vector   m_tmp_digits;
    mpfx              m_one;
    mpn_manager       m_mpn_manager;
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@ -52,10 +52,14 @@ Revision History:
 // This is needed for _tzcnt_u32 and friends.
 #include <immintrin.h>
 #define _trailing_zeros32(X) _tzcnt_u32(X)
-#endif
-
-#if defined(__GNUC__)
+#elif defined(__GNUC__)
 #define _trailing_zeros32(X) __builtin_ctz(X)
+#else
+static uint32_t _trailing_zeros32(uint32_t x) {
+    uint32_t r = 0;
+    for (; 0 == (x & 1) && r < 32; ++r, x >>= 1);
+    return r;
+}
 #endif

 #if (defined(__LP64__) || defined(_WIN64)) && !defined(_M_ARM) && !defined(_M_ARM64)
@ -65,23 +69,11 @@ Revision History:
 #define _trailing_zeros64(X) _tzcnt_u64(X)
 #endif
 #else
-inline uint64_t _trailing_zeros64(uint64_t x) {
+static uint64_t _trailing_zeros64(uint64_t x) {
    uint64_t r = 0;
    for (; 0 == (x & 1) && r < 64; ++r, x >>= 1);
    return r;
 }
-
-#if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
-// _trailing_zeros32 already defined using intrinsics
-#elif defined(__GNUC__)
-// _trailing_zeros32 already defined using intrinsics
-#else
-inline uint32_t _trailing_zeros32(uint32_t x) {
-    uint32_t r = 0;
-    for (; 0 == (x & 1) && r < 32; ++r, x >>= 1);
-    return r;
-}
-#endif
 #endif

 unsigned trailing_zeros(uint32_t x) {
@ -1723,8 +1715,8 @@ void mpz_manager<SYNCH>::display(std::ostream & out, mpz const & a) const {
        // GMP version
        size_t sz = mpz_sizeinbase(*a.m_ptr, 10) + 2;
        sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 10, *a.m_ptr);
-        out << buffer.c_ptr();
+        mpz_get_str(buffer.data(), 10, *a.m_ptr);
+        out << buffer.data();
 #endif
    } 
 }
@ -1783,11 +1775,11 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
        unsigned requiredLength = num_bits / 4;
        unsigned padding = requiredLength > sz ? requiredLength - sz : 0;
        sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr));
+        mpz_get_str(buffer.data(), 16, *(a.m_ptr));
        for (unsigned i = 0; i < padding; ++i) {
            out << "0";
        }
-        out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0);
+        out << buffer.data() + (sz > requiredLength ? sz - requiredLength : 0);
 #endif
    }
    out.copyfmt(fmt);
@ -1837,11 +1829,11 @@ void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned
        size_t sz = mpz_sizeinbase(*(a.m_ptr), 2);
        unsigned padding = num_bits > sz ? num_bits - sz : 0;
        sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr));
+        mpz_get_str(buffer.data(), 2, *(a.m_ptr));
        for (unsigned i = 0; i < padding; ++i) {
            out << "0";
        }
-        out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0);
+        out << buffer.data() + (sz > num_bits ? sz - num_bits : 0);
 #endif
    }
 }
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@ -58,28 +58,28 @@ public:
    ref_vector_core(ref_vector_core &&) noexcept = default;
    
    ~ref_vector_core() {
-        dec_range_ref(m_nodes.begin(), m_nodes.end());
+        dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
    }
    
    void reset() {
-        dec_range_ref(m_nodes.begin(), m_nodes.end());
+        dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
        m_nodes.reset();
    }

    void finalize() {
-        dec_range_ref(m_nodes.begin(), m_nodes.end());
+        dec_range_ref(m_nodes.data(), m_nodes.data() + m_nodes.size());
        m_nodes.finalize();
    }

    void resize(unsigned sz) {
        if (sz < m_nodes.size())
-            dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
+            dec_range_ref(m_nodes.data() + sz, m_nodes.data() + m_nodes.size());
        m_nodes.resize(sz);
    }

    void resize(unsigned sz, T * d) {
        if (sz < m_nodes.size()) {
-            dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
+            dec_range_ref(m_nodes.data() + sz, m_nodes.data() + m_nodes.size());
            m_nodes.shrink(sz); 
        }
        else {
@ -130,11 +130,11 @@ public:

    T * get(unsigned idx, T * d) const { return m_nodes.get(idx, d); }

-    T * const * data() const { return m_nodes.begin(); }
+    T * const * data() const { return m_nodes.data(); }

    typedef T* const* iterator;

-    T ** data() { return m_nodes.begin(); }
+    T ** data() { return m_nodes.data(); }

    unsigned hash() const {
        unsigned sz = size();
--- a/src/util/scoped_numeral_vector.h
+++ b/src/util/scoped_numeral_vector.h
@ -39,7 +39,7 @@ public:
    }

    void reset() {
-        unsigned sz = this->size();
+        auto sz = this->size();
        for (unsigned i = 0; i < sz; i++) {
            m().del(this->operator[](i));
        }
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@ -80,7 +80,7 @@ public:

    // Insert in the this object the elements in the set source.
    uint_set & operator |=(const uint_set & source) {
-        unsigned source_size = source.size();
+        auto source_size = source.size();
        if (source_size > size()) {
            resize(source_size + 1);
        }
@ -91,7 +91,7 @@ public:
    }

    uint_set& operator &=(const uint_set& source) {
-        unsigned source_size = source.size();
+        auto source_size = source.size();
        if (source_size < size()) {
            resize(source_size);
        }
@ -102,7 +102,7 @@ public:
    }

    bool operator==(const uint_set & source) const {
-        unsigned min_size = size();
+        auto min_size = size();
        if (source.size() < min_size) {
            min_size = source.size();
        }
@ -111,12 +111,12 @@ public:
                return false;
            }
        }
-        for (unsigned i = min_size; i < size(); ++i) {
+        for (auto i = min_size; i < size(); ++i) {
            if ((*this)[i]) {
                return false;
            }
        }
-        for (unsigned i = min_size; i < source.size(); ++i) {
+        for (auto i = min_size; i < source.size(); ++i) {
            if (source[i]) {
                return false;
            }
@ -131,7 +131,7 @@ public:

    // Return true if the this set is a subset of source.
    bool subset_of(const uint_set & source) const {
-        unsigned min_size = size();
+        auto min_size = size();
        if (source.size() < min_size) {
            min_size = source.size();
        }
@ -140,7 +140,7 @@ public:
                return false;
            }
        }
-        for (unsigned i = min_size; i < size(); ++i) {
+        for (auto i = min_size; i < size(); ++i) {
            if ((*this)[i]) {
                return false;
            }
@ -252,7 +252,7 @@ public:
    void remove(unsigned v) {
        if (contains(v)) {
            m_in_set[v] = false;
-            unsigned i = m_set.size();
+            auto i = m_set.size();
            for (; i > 0 && m_set[--i] != v; ) 
                ;
            SASSERT(m_set[i] == v);
@ -282,7 +282,7 @@ public:
    iterator end() const { return m_set.end(); }
    // void reset() { m_set.reset(); m_in_set.reset(); }
    void reset() { 
-        unsigned sz = m_set.size();
+        auto sz = m_set.size();
        for (unsigned i = 0; i < sz; ++i) m_in_set[m_set[i]] = false;
        m_set.reset(); 
    }
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@ -134,6 +134,14 @@ public:
        CASSERT("union_find", check_invariant());
    }

+    void set_root(unsigned v, unsigned root) {
+        TRACE("union_find", tout << "merging " << v << " " << root << "\n";);
+        SASSERT(v != root);
+        m_find[v] = root;
+        m_size[root] += m_size[v];
+        std::swap(m_next[root], m_next[v]);
+    }
+
    // dissolve equivalence class of v
    // this method cannot be used with backtracking.
    void dissolve(unsigned v) {
--- a/src/util/vector.h
+++ b/src/util/vector.h
@ -40,6 +40,125 @@ Revision History:
 #pragma warning(disable:4127)
 #endif

+
+#if 0
+
+// portability guide to std::vector.
+// memory allocator should be based on memory_allocator<T>
+// 
+// template<typename T>
+// struct memory_allocator {
+//     typedef  T value_type;
+//     etc (interface seems to change between C++17, 20 versions)
+// };
+//
+
+// Note:
+// polynomial.h contains declaration
+// typedef svector<numeral>                        numeral_vector;
+// it is crucial that it uses svector and not vector. The destructors on elements of the numeral vector are handled outside.
+// Numeral gets instantiated by mpz and mpz does not support copy constructors.
+// porting svector to vector is therefore blocked on the semantics of svector being 
+// copy-constructor free.
+// 
+
+#include <vector>
+
+template<typename T, bool CallDestructors=true, typename SZ = unsigned>
+class vector : public std::vector<T> {
+public:
+    typedef T data_t;
+    typedef typename std::vector<T>::iterator iterator;
+
+    vector() {}
+    vector(SZ s) {
+        // TODO resize(s, T());
+    }
+    vector(SZ s, T const& e) {
+        // TODO resize(s, e);
+    }
+
+    vector(SZ s, T const* e) {
+        // TODO
+    }
+
+    void reset() { clear(); }
+    void finalize() { clear(); }
+    void reserve(SZ s, T const & d) {
+        if (s > size())
+            resize(s, d);
+    }
+    void reserve(SZ s) {
+        
+    }
+
+    void setx(SZ idx, T const & elem, T const & d) {
+        if (idx >= size()) 
+            resize(idx+1, d);
+        (*this)[idx] = elem;
+    }
+
+    T const & get(SZ idx, T const & d) const {
+        if (idx >= size()) {
+            return d;
+        }
+        return (*this)[idx];
+    }
+
+    void insert(T const & elem) {
+        push_back(elem);
+    }
+    
+    void erase(iterator pos) {
+        // TODO
+    }
+
+    void erase(T const& e) {
+        // TODO
+    }
+    void fill(T const & elem) {
+        for (auto& e : *this)
+            e = elem;
+    }
+
+    void fill(unsigned sz, T const & elem) {
+        resize(sz);
+        fill(elem);
+    }
+
+    void shrink(SZ s) {
+        resize(s);
+    }
+    void reverse() {
+        SZ sz = size();
+        for (SZ i = 0; i < sz/2; ++i) {
+            std::swap((*this)[i], (*this)[sz-i-1]);
+        }
+    }
+
+    void append(vector<T, CallDestructors> const & other) {
+        for(SZ i = 0; i < other.size(); ++i) {
+            push_back(other[i]);
+        }
+    }
+
+    void append(unsigned n,  T const* elems) {
+        // TODO
+    }
+
+    bool contains(T const & elem) const {
+        for (auto const& e : *this)
+            if (e == elem)
+                return true;
+        return false;
+    }
+
+    
+}; 
+
+
+#else
+
 template<typename T, bool CallDestructors=true, typename SZ = unsigned>
 class vector {
 #define SIZE_IDX     -1
@ -602,6 +721,8 @@ public:

 };

+#endif
+
 template<typename T>
 class ptr_vector : public vector<T *, false> {
 public: