Merge remote-tracking branch 'origin/master' into polysat

2025-04-22 16:45:31 +00:00 · 2023-12-18 10:18:05 +01:00 · 2023-12-18 10:18:05 +01:00 · 734c44b004
commit 734c44b004
parent c45eb2a870 2f2bf749b9
126 changed files with 2244 additions and 308 deletions
--- a/src/api/python/setup.py
+++ b/src/api/python/setup.py
@ -313,6 +313,8 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
            osver = RELEASE_METADATA[3]
            if osver.count('.') > 1:
                osver = '.'.join(osver.split('.')[:2])
+            if osver.startswith("11"):
+                osver = "11_0"
            if arch == 'x64':
                plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
            elif arch == 'arm64':
@ -339,6 +341,7 @@ setup(
    license='MIT License',
    keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
    packages=['z3'],
+    install_requires = ['importlib-resources'],
    include_package_data=True,
    package_data={
        'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@ -508,6 +508,19 @@ static bool is_const_op(decl_kind k) {
        //k == OP_0_PW_0_REAL;
 }

+symbol arith_decl_plugin::bv_symbol(decl_kind k) const {
+    switch (k) {
+    case OP_ARITH_BAND: return symbol("band");
+    case OP_ARITH_SHL: return symbol("shl");
+    case OP_ARITH_ASHR: return symbol("ashr");
+    case OP_ARITH_LSHR: return symbol("lshr");
+    default:
+        UNREACHABLE();
+    }
+    return symbol();
+}
+
+
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                          unsigned arity, sort * const * domain, sort * range) {
    if (k == OP_NUM)
@ -523,6 +536,12 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
        return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                       func_decl_info(m_family_id, k, num_parameters, parameters));
    }
+    if (k == OP_ARITH_BAND || k == OP_ARITH_SHL || k == OP_ARITH_ASHR || k == OP_ARITH_LSHR) {
+        if (arity != 2 || domain[0] != m_int_decl || domain[1] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) 
+            m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer");
+        return m_manager->mk_func_decl(bv_symbol(k), 2, domain, m_int_decl,
+            func_decl_info(m_family_id, k, num_parameters, parameters));
+    }

    if (m_manager->int_real_coercions() && use_coercion(k)) {
        return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
@ -548,6 +567,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
        return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                       func_decl_info(m_family_id, k, num_parameters, parameters));
    }
+    if (k == OP_ARITH_BAND  || k == OP_ARITH_SHL || k == OP_ARITH_ASHR || k == OP_ARITH_LSHR) {
+        if (num_args != 2 || args[0]->get_sort() != m_int_decl || args[1]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int())
+            m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer");
+        sort* domain[2] = { m_int_decl, m_int_decl };
+        return m_manager->mk_func_decl(bv_symbol(k), 2, domain, m_int_decl,
+            func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+
    if (m_manager->int_real_coercions() && use_coercion(k)) {
        return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
    }
@ -693,7 +720,16 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
    return mk_numeral(rational(0), s == m_int_decl);
 }

-bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
+bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const {
+    if (is_irrational_algebraic_numeral(n)) {
+        scoped_anum an(am());
+        is_irrational_algebraic_numeral2(n, an);
+        if (am().is_rational(an)) {
+            am().to_rational(an, val);
+            is_int = val.is_int();
+            return true;
+        }
+    }
    if (!is_app_of(n, arith_family_id, OP_NUM))
        return false;
    func_decl * decl = to_app(n)->get_decl();
@ -724,7 +760,7 @@ bool arith_recognizers::is_int_expr(expr const *e) const {
        if (is_to_real(e)) {
            // pass
        }
-        else if (is_numeral(e, r) && r.is_int()) {
+        else if (is_numeral(e) && is_int(e)) {
            // pass
        }
        else if (is_add(e) || is_mul(e)) {
@ -747,14 +783,14 @@ void arith_util::init_plugin() {
    m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(arith_family_id));
 }

-bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
+bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const {
    if (!is_app_of(n, arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM))
        return false;
    am().set(val, to_irrational_algebraic_numeral(n));
    return true;
 }

-algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) {
+algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) const {
    SASSERT(is_irrational_algebraic_numeral(n));
    return plugin().aw().to_anum(to_app(n)->get_decl());
 }
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@ -70,6 +70,11 @@ enum arith_op_kind {
    OP_ASINH,
    OP_ACOSH,
    OP_ATANH,
+    // Bit-vector functions
+    OP_ARITH_BAND,
+    OP_ARITH_SHL,
+    OP_ARITH_ASHR,
+    OP_ARITH_LSHR,
    // constants
    OP_PI,
    OP_E,
@ -148,6 +153,8 @@ protected:

    bool        m_convert_int_numerals_to_real;

+    symbol bv_symbol(decl_kind k) const;
+
    func_decl * mk_func_decl(decl_kind k, bool is_real);
    void set_manager(ast_manager * m, family_id id) override;
    decl_kind fix_kind(decl_kind k, unsigned arity);
@ -231,30 +238,22 @@ public:
   executed in different threads.
 */
 class arith_recognizers {
+    bool is_arith_op(expr const* n, decl_kind k, unsigned& sz, expr*& x, expr*& y) {
+        if (!is_app_of(n, arith_family_id, k))
+            return false;
+        x = to_app(n)->get_arg(0);
+        y = to_app(n)->get_arg(1);
+        sz = to_app(n)->get_parameter(0).get_int();
+        return true;
+    }
 public:
    family_id get_family_id() const { return arith_family_id; }

    bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == arith_family_id; }
-    bool is_irrational_algebraic_numeral(expr const * n) const;
-    bool is_unsigned(expr const * n, unsigned& u) const { 
-        rational val;
-        bool is_int = true;
-        return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true); 
-    }
-    bool is_numeral(expr const * n, rational & val, bool & is_int) const;
-    bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
-    bool is_numeral(expr const * n) const { return is_app_of(n, arith_family_id, OP_NUM); }
-    bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
-    bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
-    // return true if \c n is a term of the form (* -1 r)
-    bool is_times_minus_one(expr * n, expr * & r) const {
-        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
-            r = to_app(n)->get_arg(1);
-            return true;
-        }
-        return false;
-    }

+    bool is_irrational_algebraic_numeral(expr const* n) const;
+
+    bool is_numeral(expr const* n) const { return is_app_of(n, arith_family_id, OP_NUM); }
    bool is_int_expr(expr const * e) const;

    bool is_le(expr const * n) const { return is_app_of(n, arith_family_id, OP_LE); }
@ -309,6 +308,15 @@ public:
    bool is_int_real(sort const * s) const { return s->get_family_id() == arith_family_id; }
    bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }

+    bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); }
+    bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_BAND, sz, x, y); }
+    bool is_shl(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_SHL); }
+    bool is_shl(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_SHL, sz, x, y); }
+    bool is_lshr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_LSHR); }
+    bool is_lshr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_LSHR, sz, x, y); }
+    bool is_ashr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_ASHR); }
+    bool is_ashr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_ASHR, sz, x, y); }
+
    bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); }
    bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); }
    bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); }
@ -387,13 +395,32 @@ public:
        return *m_plugin;
    }

-    algebraic_numbers::manager & am() {
+    algebraic_numbers::manager & am() const {
        return plugin().am();
    }

+    // return true if \c n is a term of the form (* -1 r)
+    bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
+    bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
+    bool is_times_minus_one(expr* n, expr*& r) const {
+        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
+            r = to_app(n)->get_arg(1);
+            return true;
+        }
+        return false;
+    }
+    bool is_unsigned(expr const* n, unsigned& u) const {
+        rational val;
+        bool is_int = true;
+        return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true);
+    }
+    bool is_numeral(expr const* n) const { return arith_recognizers::is_numeral(n); }
+    bool is_numeral(expr const* n, rational& val, bool& is_int) const;
+    bool is_numeral(expr const* n, rational& val) const { bool is_int; return is_numeral(n, val, is_int); }
+
    bool convert_int_numerals_to_real() const { return plugin().convert_int_numerals_to_real(); }
-    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
-    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
+    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const;
+    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n) const;

    sort * mk_int() { return m_manager.mk_sort(arith_family_id, INT_SORT); }
    sort * mk_real() { return m_manager.mk_sort(arith_family_id, REAL_SORT); }
@ -471,6 +498,11 @@ public:
    app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); }
    app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); }

+    app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); }
+    app* mk_shl(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, 2, args); }
+    app* mk_ashr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, 2, args); }
+    app* mk_lshr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, 2, args); }
+
    app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); }
    app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); }
    app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); }
@ -498,11 +530,11 @@ public:
       if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
    */
    app * mk_eq(expr * lhs, expr * rhs) {
-        if (is_numeral(lhs) || (!is_numeral(rhs) && lhs->get_id() > rhs->get_id()))
+        if (arith_recognizers::is_numeral(lhs) || (!arith_recognizers::is_numeral(rhs) && lhs->get_id() > rhs->get_id()))
            std::swap(lhs, rhs);
        if (lhs == rhs)
            return m_manager.mk_true();
-        if (is_numeral(lhs) && is_numeral(rhs)) {
+        if (arith_recognizers::is_numeral(lhs) && arith_recognizers::is_numeral(rhs)) {
            SASSERT(lhs != rhs);
            return m_manager.mk_false();
        }
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@ -942,3 +942,8 @@ app * bv_util::mk_bv2int(expr* e) {
    parameter p(s);
    return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
 }
+
+app* bv_util::mk_int2bv(unsigned sz, expr* e) {
+    parameter p(sz);
+    return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e);
+}
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@ -386,9 +386,31 @@ public:
    bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
    bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
    bool is_bv_umul_no_ovfl(expr const* e) const { return is_app_of(e, get_fid(), OP_BUMUL_NO_OVFL); }
+    bool is_redand(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDAND); }
+    bool is_redor(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDOR); }
+    bool is_comp(expr const* e) const { return is_app_of(e, get_fid(), OP_BCOMP); }
+    bool is_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_LEFT); }
+    bool is_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_RIGHT); }
+    bool is_ext_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_LEFT); }
+    bool is_ext_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_RIGHT); }
+
+    bool is_rotate_left(expr const* e, unsigned& n, expr*& x) const {
+        return is_rotate_left(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }
+    bool is_rotate_right(expr const* e, unsigned& n, expr*& x) const {
+        return is_rotate_right(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }
+    bool is_int2bv(expr const* e, unsigned& n, expr*& x) const {
+        return is_int2bv(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }

    MATCH_UNARY(is_bv_not);
+    MATCH_UNARY(is_redand);
+    MATCH_UNARY(is_redor);

+    MATCH_BINARY(is_ext_rotate_left);
+    MATCH_BINARY(is_ext_rotate_right);
+    MATCH_BINARY(is_comp);
    MATCH_BINARY(is_bv_add);
    MATCH_BINARY(is_bv_sub);
    MATCH_BINARY(is_bv_mul);
@ -411,6 +433,12 @@ public:
    MATCH_BINARY(is_bv_sdiv);
    MATCH_BINARY(is_bv_udiv);
    MATCH_BINARY(is_bv_smod);
+    MATCH_BINARY(is_bv_and);
+    MATCH_BINARY(is_bv_or);
+    MATCH_BINARY(is_bv_xor);
+    MATCH_BINARY(is_bv_nand);
+    MATCH_BINARY(is_bv_nor);
+

    MATCH_BINARY(is_bv_uremi);
    MATCH_BINARY(is_bv_sremi);
@ -516,6 +544,7 @@ public:
    app * mk_bv_lshr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BLSHR, arg1, arg2); }

    app * mk_bv2int(expr* e);
+    app * mk_int2bv(unsigned sz, expr* e);

    // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return`
    app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); }
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@ -400,6 +400,7 @@ class bv_expr_inverter : public iexpr_inverter {
    }

    bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+//        return false;
        if (num == 0)
            return false;
        if (!uncnstr(num, args))
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@ -104,8 +104,8 @@ namespace euf {
    }

    void bv_plugin::merge_eh(enode* x, enode* y) {
-        SASSERT(x == x->get_root());
-        SASSERT(x == y->get_root());
+        if (!bv.is_bv(x->get_expr()))
+            return;

        TRACE("bv", tout << "merge_eh " << g.bpp(x) << " == " << g.bpp(y) << "\n");
        SASSERT(!m_internal);
@ -343,7 +343,8 @@ namespace euf {
        enode* hi = mk_extract(n, cut, w - 1);
        enode* lo = mk_extract(n, 0, cut - 1);        
        auto& i = info(n);
-        SASSERT(i.value);
+        if (!i.value)
+            i.value = n;
        i.hi = hi;
        i.lo = lo;
        i.cut = cut;
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@ -2189,7 +2189,13 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
    renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
    SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2);
    res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
-    res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
+    if (sbits >= ebits+2)
+        res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
+    else {
+        // should not overflow because renorm_delta is logarithmic to the size of the leading zero bits
+        res_sig = m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+2-sbits, res_sig), renorm_delta);
+        res_sig = m_bv_util.mk_extract(sbits-1, 0, res_sig);
+    }
    dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta);
    dbg_decouple("fpa2bv_r2i_sig_lz", sig_lz);
    dbg_decouple("fpa2bv_r2i_sig_lz_capped", sig_lz_capped);
--- a/src/ast/polymorphism_inst.cpp
+++ b/src/ast/polymorphism_inst.cpp
@ -94,7 +94,10 @@ namespace polymorphism {
            t.push(value_trail(m_decl_qhead));
            for (; m_decl_qhead < num_decls; ++m_decl_qhead) {
                func_decl* p = m_decl_queue.get(m_decl_qhead);
-                for (expr* e : m_occurs[m.poly_root(p)])
+                func_decl* r = m.poly_root(p);
+                if (!m_occurs.contains(r))
+                    continue;
+                for (expr* e : m_occurs[r])
                    instantiate(p, e, instances);
            }
        }
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@ -602,15 +602,6 @@ namespace recfun {
        m_args.append(n->get_num_args(), n->get_args());
    }

-    case_expansion::case_expansion(case_expansion const & from)
-        : m_lhs(from.m_lhs),
-          m_def(from.m_def),
-          m_args(from.m_args) {}
-    case_expansion::case_expansion(case_expansion && from)
-        : m_lhs(from.m_lhs),
-          m_def(from.m_def),
-          m_args(std::move(from.m_args)) {}
-
    std::ostream& case_expansion::display(std::ostream & out) const {
        return out << "case_exp(" << m_lhs << ")";
    }
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@ -301,8 +301,6 @@ namespace recfun {
        recfun::def *       m_def;
        expr_ref_vector     m_args;
        case_expansion(recfun::util& u, app * n);
-        case_expansion(case_expansion const & from);
-        case_expansion(case_expansion && from);
        std::ostream& display(std::ostream& out) const;
    };

@ -323,10 +321,6 @@ namespace recfun {
        }
        body_expansion(app_ref & pred, recfun::case_def const & d, expr_ref_vector & args) : 
            m_pred(pred), m_cdef(&d), m_args(args) {}
-        body_expansion(body_expansion const & from): 
-            m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
-        body_expansion(body_expansion && from) noexcept :
-            m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}

        std::ostream& display(std::ostream& out) const;
    };
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@ -91,6 +91,10 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
    case OP_SINH: SASSERT(num_args == 1); st = mk_sinh_core(args[0], result); break;
    case OP_COSH: SASSERT(num_args == 1); st = mk_cosh_core(args[0], result); break;
    case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break;
+    case OP_ARITH_BAND: SASSERT(num_args == 2);  st = mk_band_core(f->get_parameter(0).get_int(), args[0], args[1], result); break;
+    case OP_ARITH_SHL: SASSERT(num_args == 2);  st = mk_shl_core(f->get_parameter(0).get_int(), args[0], args[1], result); break;
+    case OP_ARITH_ASHR: SASSERT(num_args == 2);  st = mk_ashr_core(f->get_parameter(0).get_int(), args[0], args[1], result); break;
+    case OP_ARITH_LSHR: SASSERT(num_args == 2);  st = mk_lshr_core(f->get_parameter(0).get_int(), args[0], args[1], result); break;
    default: st = BR_FAILED; break;
    }
    CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m);
@ -1228,19 +1232,20 @@ static rational symmod(rational const& a, rational const& b) {
    
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
    set_curr_sort(arg1->get_sort());
-    numeral v1, v2;
-    bool is_int;
-    if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
-        result = m_util.mk_numeral(mod(v1, v2), is_int);
+    numeral x, y;
+    bool is_num_x = m_util.is_numeral(arg1, x);
+    bool is_num_y = m_util.is_numeral(arg2, y);
+    if (is_num_x && is_num_y && !y.is_zero()) {
+        result = m_util.mk_int(mod(x, y));
        return BR_DONE;
    }

-    if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) {
+    if (is_num_y && y.is_int() && (y.is_one() || y.is_minus_one())) {
        result = m_util.mk_numeral(numeral(0), true);
        return BR_DONE;
    }

-    if (arg1 == arg2 && !m_util.is_numeral(arg2)) {
+    if (arg1 == arg2 && !is_num_y) {
        expr_ref zero(m_util.mk_int(0), m);
        result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero);
        return BR_DONE;
@ -1248,29 +1253,35 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul

    // mod is idempotent on non-zero modulus.
    expr* t1, *t2;
-    if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
+    if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && is_num_y && y.is_int() && !y.is_zero()) {
+        result = arg1;
+        return BR_DONE;
+    }
+
+    rational lo, hi;
+    if (is_num_y && get_range(arg1, lo, hi) && 0 <= lo && hi < y) {
        result = arg1;
        return BR_DONE;
    }

    // propagate mod inside only if there is something to reduce.
-    if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) {
+    if (is_num_y && y.is_int() && y.is_pos() && (is_add(arg1) || is_mul(arg1))) {
        TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";);
        expr_ref_buffer args(m);
        bool change = false;
        for (expr* arg : *to_app(arg1)) {
            rational arg_v;
-            if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) != arg_v) {
+            if (m_util.is_numeral(arg, arg_v) && mod(arg_v, y) != arg_v) {
                change = true;
-                args.push_back(m_util.mk_numeral(mod(arg_v, v2), true));
+                args.push_back(m_util.mk_numeral(mod(arg_v, y), true));
            }
            else if (m_util.is_mod(arg, t1, t2) && t2 == arg2) {
                change = true;
                args.push_back(t1);
            }
-            else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) {
+            else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, y) != arg_v) {
                change = true;
-                args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2));
+                args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, y), true), t2));
            }
            else {
                args.push_back(arg);
@ -1287,6 +1298,27 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
    return BR_FAILED;
 }

+bool arith_rewriter::get_range(expr* e, rational& lo, rational& hi) {
+    expr* x, *y;
+    rational r;
+    if (m_util.is_idiv(e, x, y) && m_util.is_numeral(y, r) && get_range(x, lo, hi) && 0 <= lo && r > 0) {
+        lo = div(lo, r);
+        hi = div(hi, r);
+        return true;
+    }
+    if (m_util.is_mod(e, x, y) && m_util.is_numeral(y, r) && r > 0) {
+        lo = 0;
+        hi = r - 1;
+        return true;
+    }
+    if (m_util.is_numeral(e, r)) {
+        lo = hi = r;
+        return true;
+    }
+    return false;
+}
+
+
 br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & result) {
    set_curr_sort(arg1->get_sort());
    numeral v1, v2;
@ -1349,6 +1381,134 @@ app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) {
    return y;
 }

+br_status arith_rewriter::mk_shl_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) {
+    numeral x, y, N;
+    bool is_num_x = m_util.is_numeral(arg1, x);
+    bool is_num_y = m_util.is_numeral(arg2, y);
+    N = rational::power_of_two(sz);
+    if (is_num_x) 
+        x = mod(x, N);
+    if (is_num_y)
+        y = mod(y, N);
+    if (is_num_x && is_num_y) {
+        if (y >= sz) 
+            result = m_util.mk_int(0);
+        else 
+            result = m_util.mk_int(mod(x * rational::power_of_two(y.get_unsigned()), N));
+        return BR_DONE;
+    }
+    if (is_num_y) {
+        if (y >= sz) 
+            result = m_util.mk_int(0);
+        else 
+            result = m_util.mk_mod(m_util.mk_mul(arg1, m_util.mk_int(rational::power_of_two(y.get_unsigned()))), m_util.mk_int(N));
+        return BR_REWRITE1;
+    }
+    if (is_num_x && x == 0) {
+        result = m_util.mk_int(0);
+        return BR_DONE;
+    }        
+    return BR_FAILED;
+}
+br_status arith_rewriter::mk_ashr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) {
+    numeral x, y, N;
+    bool is_num_x = m_util.is_numeral(arg1, x);
+    bool is_num_y = m_util.is_numeral(arg2, y);
+    N = rational::power_of_two(sz);
+    if (is_num_x) 
+        x = mod(x, N);
+    if (is_num_y)
+        y = mod(y, N);
+    if (is_num_x && x == 0) {
+        result = m_util.mk_int(0);
+        return BR_DONE;
+    }
+    if (is_num_x && is_num_y) {
+        bool signx = x >= N/2;
+        rational d = div(x, rational::power_of_two(y.get_unsigned()));
+        SASSERT(y >= 0);
+        if (signx) {
+            if (y >= sz)
+                result = m_util.mk_int(N-1);
+            else
+                result = m_util.mk_int(d);
+        }
+        else {
+            if (y >= sz) 
+                result = m_util.mk_int(0);
+            else 
+                result = m_util.mk_int(mod(d - rational::power_of_two(sz - y.get_unsigned()), N));
+        }
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) {
+    numeral x, y, N;
+    bool is_num_x = m_util.is_numeral(arg1, x);
+    bool is_num_y = m_util.is_numeral(arg2, y);
+    N = rational::power_of_two(sz);
+    if (is_num_x) 
+        x = mod(x, N);
+    if (is_num_y)
+        y = mod(y, N);
+    if (is_num_x && x == 0) {
+        result = m_util.mk_int(0);
+        return BR_DONE;
+    }
+    if (is_num_y && y == 0) {
+        result = arg1;
+        return BR_DONE;
+    }
+    if (is_num_x && is_num_y) {
+        if (y >= sz)
+            result = m_util.mk_int(0);
+        else {
+            rational d = div(x, rational::power_of_two(y.get_unsigned()));
+            result = m_util.mk_int(d);
+        }
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status arith_rewriter::mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) {
+    numeral x, y, N;
+    bool is_num_x = m_util.is_numeral(arg1, x);
+    bool is_num_y = m_util.is_numeral(arg2, y);
+    N = rational::power_of_two(sz);
+    if (is_num_x) 
+        x = mod(x, N);      
+    if (is_num_y)
+        y = mod(y, N);
+    if (is_num_x && x.is_zero()) {
+        result = m_util.mk_int(0);
+        return BR_DONE;
+    }
+    if (is_num_y && y.is_zero()) {
+        result = m_util.mk_int(0);
+        return BR_DONE;
+    }
+    if (is_num_x && is_num_y) {
+        rational r(0);
+        for (unsigned i = 0; i < sz; ++i)
+            if (x.get_bit(i) && y.get_bit(i))
+                r += rational::power_of_two(i);
+        result = m_util.mk_int(r);
+        return BR_DONE;
+    }
+    if (is_num_x && (x + 1).is_power_of_two()) {
+        result = m_util.mk_mod(arg2, m_util.mk_int(x + 1));
+        return BR_REWRITE1;
+    }
+    if (is_num_y && (y + 1).is_power_of_two()) {
+        result = m_util.mk_mod(arg1, m_util.mk_int(y + 1));
+        return BR_REWRITE1;
+    }
+    return BR_FAILED;
+}
+
 br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) {
    numeral x, y;
    bool is_num_x    = m_util.is_numeral(arg1, x);
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@ -63,6 +63,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
    bool m_eq2ineq;
    unsigned m_max_degree;

+    bool get_range(expr* e, rational& lo, rational& hi);
    void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts);
    enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE };
    bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result);
@ -159,6 +160,10 @@ public:
    br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);
    br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result);
    br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result);
+    br_status mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result);
+    br_status mk_shl_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result);
+    br_status mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result);
+    br_status mk_ashr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result);
    void mk_div(expr * arg1, expr * arg2, expr_ref & result) {
        if (mk_div_core(arg1, arg2, result) == BR_FAILED)
            result = m.mk_app(get_fid(), OP_DIV, arg1, arg2);
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@ -105,14 +105,14 @@ public:
 class default_dependent_expr_state : public dependent_expr_state {
 public:
    default_dependent_expr_state(ast_manager& m): dependent_expr_state(m) {}
-    virtual unsigned qtail() const { return 0; }
-    virtual dependent_expr const& operator[](unsigned i) { throw default_exception("unexpected access"); }
-    virtual void update(unsigned i, dependent_expr const& j) { throw default_exception("unexpected update"); }
-    virtual void add(dependent_expr const& j) { throw default_exception("unexpected addition"); }
-    virtual bool inconsistent() { return false; }
-    virtual model_reconstruction_trail& model_trail() { throw default_exception("unexpected access to model reconstruction"); }
-    virtual bool updated() { return false; }
-    virtual void reset_updated() {}
+    unsigned qtail() const override { return 0; }
+    dependent_expr const& operator[](unsigned i) override { throw default_exception("unexpected access"); }
+    void update(unsigned i, dependent_expr const& j) override { throw default_exception("unexpected update"); }
+    void add(dependent_expr const& j) override { throw default_exception("unexpected addition"); }
+    bool inconsistent() override { return false; }
+    model_reconstruction_trail& model_trail() override { throw default_exception("unexpected access to model reconstruction"); }
+    bool updated() override { return false; }
+    void reset_updated() override {}

 };

--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@ -66,7 +66,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const {
 }

 void elim_unconstrained::eliminate() {
-
    while (!m_heap.empty()) {
        expr_ref r(m);
        int v = m_heap.erase_min();
@ -86,7 +85,12 @@ void elim_unconstrained::eliminate() {
            n.m_refcount = 0;
            continue;
        }
+        if (m_heap.contains(root(e))) {
+            IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
+            continue;
+        }
        app* t = to_app(e);
+        TRACE("elim_unconstrained", tout << "eliminating " << mk_pp(t, m) << "\n";);
        unsigned sz = m_args.size();
        for (expr* arg : *to_app(t))
            m_args.push_back(reconstruct_term(get_node(arg)));
@ -99,12 +103,15 @@ void elim_unconstrained::eliminate() {
            proof * pr  = m.mk_apply_def(s, r, pr1);
            m_trail.push_back(pr);
        }
+        expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
        n.m_refcount = 0;
        m_args.shrink(sz);
        if (!inverted) {
            IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
            continue;
        }
+
+        IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
        
        TRACE("elim_unconstrained", tout << mk_pp(t, m) << " -> " << r << "\n");
        SASSERT(r->get_sort() == t->get_sort());
@ -119,7 +126,8 @@ void elim_unconstrained::eliminate() {
        get_node(e).m_term = r;
        get_node(e).m_proof = pr;
        get_node(e).m_refcount++;
-        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
+        get_node(e).m_dirty = false;
+        IF_VERBOSE(11, verbose_stream() << "set " << &get_node(e) << " " << root(e) << " " << mk_bounded_pp(e, m) << " := " << mk_bounded_pp(r, m) << "\n");
        SASSERT(!m_heap.contains(root(e)));
        if (is_uninterp_const(r))
            m_heap.insert(root(e));
@ -283,13 +291,22 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
    expr* t = n0.m_term;
    if (!n0.m_dirty)
        return expr_ref(t, m);
+    if (!is_node(t))
+        return expr_ref(t, m);
    ptr_vector<expr> todo;
    todo.push_back(t);
    while (!todo.empty()) {
        t = todo.back();
+        if (!is_node(t)) {
+            UNREACHABLE();
+        }
        node& n = get_node(t);
        unsigned sz0 = todo.size();
-        if (is_app(t)) {            
+        if (is_app(t)) {     
+            if (n.m_term != t) {
+                todo.pop_back();
+                continue;
+            }
            for (expr* arg : *to_app(t)) 
                if (get_node(arg).m_dirty || !get_node(arg).m_term)
                    todo.push_back(arg);
@ -300,7 +317,6 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
            for (expr* arg : *to_app(t)) 
                m_args.push_back(get_node(arg).m_term);            
            n.m_term = m.mk_app(to_app(t)->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz);
-
            m_args.shrink(sz);
        }
        else if (is_quantifier(t)) {
@ -410,7 +426,7 @@ void elim_unconstrained::reduce() {
    generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
    m_inverter.set_model_converter(mc.get());
    m_created_compound = true;
-    for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) {
+    for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) {
        m_created_compound = false;
        init_nodes();
        eliminate();
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@ -182,11 +182,11 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
            out << "hide " << t->m_decl->get_name() << "\n";
        else if (t->is_def()) {
            for (auto const& [f, def, dep] : t->m_defs)
-                out << f->get_name() << " <- " << mk_pp(def, m) << "\n";
+                out << "def: " << f->get_name() << " <- " << mk_pp(def, m) << "\n";
        }            
        else {
            for (auto const& [v, def] : t->m_subst->sub())
-                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";            
+                out << "sub: " << mk_pp(v, m) << " -> " << mk_pp(def, m) << "\n";
        }
        for (auto const& d : t->m_removed)
            out << "rm: " << d << "\n";
--- a/src/ast/simplifiers/model_reconstruction_trail.h
+++ b/src/ast/simplifiers/model_reconstruction_trail.h
@ -90,7 +90,7 @@ class model_reconstruction_trail {
    struct undo_model_var : public trail {
        model_reconstruction_trail& s;
        undo_model_var(model_reconstruction_trail& s) : s(s) {}
-        virtual void undo() {
+        void undo() override {
            s.m_model_vars.mark(s.m_model_vars_trail.back(), false);
            s.m_model_vars_trail.pop_back();
        }
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@ -130,6 +130,11 @@ namespace dd {
        return p + q - 2*mk_and(p, q);
    }

+    pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { 
+        pdd q(mk_val(x)); 
+        return mk_xor(p, q); 
+    }
+
    pdd pdd_manager::mk_not(pdd const& p) {
        if (m_semantics == mod2N_e)
            return -p - 1;
@ -1802,7 +1807,9 @@ namespace dd {
    pdd& pdd::operator=(pdd const& other) { 
        if (m != other.m) {
            verbose_stream() << "pdd manager confusion: " << *this << " (mod 2^" << power_of_2() << ") := " << other << " (mod 2^" << other.power_of_2() << ")\n";
+            UNREACHABLE();
            // TODO: in the end, this operator should probably be changed to also update the manager. But for now I want to detect such confusions.
+            reset(*other.m);
        }
        SASSERT_EQ(power_of_2(), other.power_of_2());
        VERIFY_EQ(power_of_2(), other.power_of_2());
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@ -347,6 +347,7 @@ namespace dd {
        pdd mk_and(pdd const& p, pdd const& q);
        pdd mk_or(pdd const& p, pdd const& q);
        pdd mk_xor(pdd const& p, pdd const& q);
+        pdd mk_xor(pdd const& p, unsigned x);
        pdd mk_not(pdd const& p);
        pdd reduce(pdd const& a, pdd const& b);
        pdd subst_val0(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
@ -502,7 +503,7 @@ namespace dd {
        unsigned max_pow2_divisor() const { return m->max_pow2_divisor(root); }
        unsigned_vector const& free_vars() const { return m->free_vars(*this); }

-        void swap(pdd& other) { VERIFY_EQ(m, other.m); std::swap(root, other.root); }
+        void swap(pdd& other) noexcept { VERIFY_EQ(m, other.m); std::swap(root, other.root); }

        pdd_iterator begin() const;
        pdd_iterator end() const;
@ -546,7 +547,7 @@ namespace dd {
    inline pdd& operator-=(pdd & p, rational const& q) { p = p - q; return p; }
    inline pdd& operator+=(pdd & p, rational const& q) { p = p + q; return p; }

-    inline void swap(pdd& p, pdd& q) { p.swap(q); }
+    inline void swap(pdd& p, pdd& q) noexcept { p.swap(q); }

    std::ostream& operator<<(std::ostream& out, pdd const& b);

--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@ -611,4 +611,19 @@ void emonics::set_propagated(monic const& m) {
    m_u_f_stack.push(set_unpropagated(*this, m.var()));
 }

+void emonics::set_bound_propagated(monic const& m) {
+    struct set_bound_unpropagated : public trail {
+        emonics& em;
+        unsigned var;
+    public:
+        set_bound_unpropagated(emonics& em, unsigned var): em(em), var(var) {}
+        void undo() override {
+            em[var].set_bound_propagated(false);
+        }
+    };
+    SASSERT(!m.is_bound_propagated());
+    (*this)[m.var()].set_bound_propagated(true);
+    m_u_f_stack.push(set_bound_unpropagated(*this, m.var()));
+}
+
 }
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@ -143,6 +143,7 @@ public:
    void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}

    void set_propagated(monic const& m);
+    void set_bound_propagated(monic const& m);

    // this method is required by union_find
    trail_stack & get_trail_stack() { return m_u_f_stack; }
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@ -409,73 +409,15 @@ lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_
    create_cut cc(t, k, ex, basic_inf_int_j, row, lia);
    return cc.cut();
 }
-
-bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
-    // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed).
-    unsigned j;
-    for (const auto & p : row) {
-        j = p.var();
-        if (!lia.is_base(j) && (!lia.at_bound(j) || !is_zero(lia.get_value(j).y))) {
-            TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
-                  lia.display_column(tout, j);
-                  tout << "infinitesimal: " << !is_zero(lia.get_value(j).y) << "\n";);
-            return false;
-        }
-    }
-    return true;
-}
-
-int gomory::find_basic_var() {
-    unsigned n = 0;
-    int result = -1;
-    unsigned min_row_size = UINT_MAX;
-
-#if 1
-    result = lia.select_int_infeasible_var(true);
-
-    if (result == -1)
-        return result;
-
-    TRACE("gomory_cut", tout << "row: " << result << "\n");
-    const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(result));
-    if (is_gomory_cut_target(row)) 
-        return result;
-    result = -1;
-
-    UNREACHABLE();
-#endif
-
-    for (unsigned j : lra.r_basis()) {
-        if (!lia.column_is_int_inf(j))
-            continue;
-        const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j));
-        TRACE("gomory_cut", tout << "try j" << j << "\n");
-        if (!is_gomory_cut_target(row)) 
-            continue;
-        IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
-        // Prefer smaller row size
-        if (min_row_size == UINT_MAX || 
-            2*row.size() < min_row_size || 
-            (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {
-            result = j;
-            n = 1;
-            min_row_size = std::min(min_row_size, row.size());
-        }
-    }
-    return result;
-}
    
-lia_move gomory::operator()() {
-    int j = find_basic_var();
-    if (j == -1)
-        return lia_move::undef;
+lia_move gomory::get_cut(lpvar j) {
    unsigned r = lia.row_of_basic_column(j);
    const row_strip<mpq>& row = lra.get_row(r);
    SASSERT(lra.row_is_correct(r));
-    SASSERT(is_gomory_cut_target(row));
+    SASSERT(lia.is_gomory_cut_target(j));
    lia.m_upper = false;
    lia.m_cut_vars.push_back(j);
-    return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);
+    return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);    
 }


--- a/src/math/lp/gomory.h
+++ b/src/math/lp/gomory.h
@ -27,11 +27,9 @@ namespace lp {
    class gomory {
        class int_solver& lia;
        class lar_solver& lra;
-        int find_basic_var();
-        bool is_gomory_cut_target(const row_strip<mpq>& row);
        lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
    public:
        gomory(int_solver& lia);
-        lia_move operator()();
+        lia_move get_cut(lpvar j);
    };
 }
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@ -53,7 +53,7 @@ lia_move int_branch::create_branch_on_column(int j) {
 int int_branch::find_inf_int_base_column() {

 #if 1
-    return lia.select_int_infeasible_var(false);
+    return lia.select_int_infeasible_var();
 #endif

    int result = -1;
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@ -198,15 +198,9 @@ namespace lp {
        if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
        if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();

-        std::function<lia_move(void)> gomory_fn = [&]() { return gomory(*this)(); };
-        m_cut_vars.reset();
-#if 0
-        if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this)();
-#else
+        std::function<lia_move(lpvar)> gomory_fn = [&](lpvar j) { return gomory(*this).get_cut(j); };
        if (r == lia_move::undef && should_gomory_cut()) r = local_cut(2, gomory_fn);
-        
-#endif
-        m_cut_vars.reset();
+
        if (r == lia_move::undef) r = int_branch(*this)();
        if (settings().get_cancel_flag()) r = lia_move::undef;        
        return r;
@ -635,7 +629,7 @@ namespace lp {
    }


-    int int_solver::select_int_infeasible_var(bool check_bounded) {
+    int int_solver::select_int_infeasible_var() {
        int r_small_box = -1;
        int r_small_value = -1;
        int r_any_value = -1;
@ -648,18 +642,6 @@ namespace lp {
        lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
        unsigned prev_usage = 0;

-        auto check_bounded_fn = [&](unsigned j) {
-            if (!check_bounded)
-                return true;
-            auto const& row = lra.get_row(row_of_basic_column(j));
-            for (const auto & p : row) {
-                unsigned j = p.var();
-                if (!is_base(j) && (!at_bound(j) || !is_zero(get_value(j).y)))
-                    return false;
-            }
-            return true;
-        };
-
        auto add_column = [&](bool improved, int& result, unsigned& n, unsigned j) {
            if (result == -1)
                result = j;
@ -670,9 +652,7 @@ namespace lp {
        for (unsigned j : lra.r_basis()) {
            if (!column_is_int_inf(j))
                continue;
-            if (!check_bounded_fn(j))
-                continue;
-            if (m_cut_vars.contains(j))
+             if (m_cut_vars.contains(j))
                continue;

            SASSERT(!is_fixed(j));
@ -849,19 +829,71 @@ namespace lp {

 #endif
    }
+    // return the minimal distance from the column value to an integer
+    mpq get_gomory_score(const int_solver& lia, lpvar j) {
+        const mpq& val = lia.get_value(j).x;
+        auto l = val - floor(val);
+        if (l <= mpq(1, 2))
+            return l;
+        return mpq(1) - l;
+    }

+    unsigned_vector int_solver::gomory_select_int_infeasible_vars(unsigned num_cuts) {
+        SASSERT(m_cut_vars.size() == 0&& num_cuts >= 0);
+        
+        std::list<lpvar> sorted_vars;
+        std::unordered_map<lpvar, mpq> score;
+        for (lpvar j : lra.r_basis()) {
+            if (!column_is_int_inf(j) || !is_gomory_cut_target(j))
+                continue;
+            SASSERT(!is_fixed(j));            
+            sorted_vars.push_back(j);
+            score[j] = get_gomory_score(*this, j);
+        }
+        // prefer the columns with the values close to integers
+        sorted_vars.sort([&](lpvar j, lpvar k) {
+            auto diff = score[j] - score[k];
+            if (diff.is_neg())
+                return true;
+            if (diff.is_pos())
+                return false;
+            return lra.usage_in_terms(j) > lra.usage_in_terms(k);
+        });
+        unsigned_vector ret;
+        unsigned n = static_cast<unsigned>(sorted_vars.size());

-    lia_move int_solver::local_cut(unsigned num_cuts, std::function<lia_move(void)>& cut_fn) {
+        while (num_cuts-- && n > 0) {
+            unsigned k = random() % n;
+           
+            double k_ratio = k / (double) n;
+            k_ratio *= k_ratio*k_ratio;  // square k_ratio to make it smaller
+            k = static_cast<unsigned>(std::floor(k_ratio * n));
+            // these operations move k to the beginning of the indices range
+            SASSERT(0 <= k && k < n);
+            auto it = sorted_vars.begin();
+            while(k--) it++;

+            ret.push_back(*it);
+            sorted_vars.erase(it);
+            n--;            
+        }
+        return ret;
+    }
+    
+    lia_move int_solver::local_cut(unsigned num_cuts, std::function<lia_move(lpvar)>& cut_fn) {
+        
        struct ex { explanation m_ex; lar_term m_term; mpq m_k; bool m_is_upper; };
+        unsigned_vector columns_for_cuts = gomory_select_int_infeasible_vars(num_cuts);
+
        vector<ex> cuts;
-        for (unsigned i = 0; i < num_cuts && has_inf_int(); ++i) {
+        
+        for (unsigned j : columns_for_cuts) {
            m_ex->clear();
            m_t.clear();
            m_k.reset();
-            auto r = cut_fn();
+            auto r = cut_fn(j);
            if (r != lia_move::cut)
-                break;
+                continue;
            cuts.push_back({ *m_ex, m_t, m_k, is_upper() });
            if (settings().get_cancel_flag())
                return lia_move::undef;
@ -938,6 +970,22 @@ namespace lp {
        return lia_move::undef;
    }

+    bool int_solver::is_gomory_cut_target(lpvar k) {
+        SASSERT(is_base(k));
+        // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed).
+        const row_strip<mpq>& row = lra.get_row(row_of_basic_column(k));
+        unsigned j;
+        for (const auto & p : row) {
+            j = p.var();
+            if ( k != j && (!at_bound(j) || !is_zero(get_value(j).y))) {
+                TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
+                      display_column(tout, j);
+                      tout << "infinitesimal: " << !is_zero(get_value(j).y) << "\n";);
+                return false;
+            }
+        }
+        return true;
+    }


 }
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@ -111,7 +111,7 @@ private:
    bool has_upper(unsigned j) const;
    unsigned row_of_basic_column(unsigned j) const;
    bool cut_indices_are_columns() const;
-    lia_move local_cut(unsigned num_cuts, std::function<lia_move(void)>& cut_fn);
+    lia_move local_cut(unsigned num_cuts, std::function<lia_move(lpvar)>& cut_fn);
        
 public:
    std::ostream& display_column(std::ostream & out, unsigned j) const;
@ -132,7 +132,8 @@ public:
    bool all_columns_are_bounded() const;
    lia_move hnf_cut();

-    int select_int_infeasible_var(bool check_bounded);
-
+    int select_int_infeasible_var();
+    unsigned_vector gomory_select_int_infeasible_vars(unsigned num_cuts);
+    bool is_gomory_cut_target(lpvar);
 };
 }
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@ -1490,7 +1490,7 @@ namespace lp {
    struct lar_solver::undo_add_column : public trail {
        lar_solver& s;
        undo_add_column(lar_solver& s) : s(s) {}
-        virtual void undo() {
+        void undo() override {
            s.remove_last_column_from_tableau();            
            s.m_columns_to_ul_pairs.pop_back();
            unsigned j = s.m_columns_to_ul_pairs.size();
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@ -532,6 +532,11 @@ public:
    inline const impq& get_lower_bound(column_index j) const {
        return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j];
    }
+
+    inline mpq bound_span_x(column_index j) const {
+        return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j].x - m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j].x;
+    }
+    
    bool has_lower_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const;
    bool has_upper_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const;
    bool has_value(var_index var, mpq& value) const;
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@ -108,6 +108,7 @@ namespace lp_api {
        unsigned m_gomory_cuts;
        unsigned m_assume_eqs;
        unsigned m_branch;
+        unsigned m_bv_axioms;
        stats() { reset(); }
        void reset() {
            memset(this, 0, sizeof(*this));
@ -128,6 +129,7 @@ namespace lp_api {
            st.update("arith-gomory-cuts", m_gomory_cuts);
            st.update("arith-assume-eqs", m_assume_eqs);
            st.update("arith-branch", m_branch);
+            st.update("arith-bv-axioms", m_bv_axioms);
        }
    };

--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@ -517,7 +517,7 @@ public:

    
    template <typename K>
-    static void swap(vector<K> &v, unsigned i, unsigned j) {
+    static void swap(vector<K> &v, unsigned i, unsigned j) noexcept {
        auto t = v[i];
        v[i] = v[j];
        v[j] = t;
--- a/src/math/lp/monic.h
+++ b/src/math/lp/monic.h
@ -59,6 +59,7 @@ class monic: public mon_eq {
    bool             m_rsign;
    mutable unsigned m_visited;
    bool             m_propagated = false;
+    bool             m_bound_propagated = false;
 public:
    // constructors
    monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):  
@ -77,6 +78,8 @@ public:
    void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
    void set_propagated(bool p) { m_propagated = p; }
    bool is_propagated() const { return m_propagated; }
+    void set_bound_propagated(bool p) { m_bound_propagated = p; }
+    bool is_bound_propagated() const { return m_bound_propagated; }
    
    svector<lpvar>::const_iterator begin() const { return vars().begin(); }
    svector<lpvar>::const_iterator end() const { return vars().end(); }
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@ -1517,6 +1517,9 @@ void core::add_bounds() {
        for (lpvar j : m.vars()) {
            if (!var_is_free(j))
                continue;
+	    if (m.is_bound_propagated())
+                continue;
+	    m_emons.set_bound_propagated(m);
            // split the free variable (j <= 0, or j > 0), and return
            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
            TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n");                  
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@ -358,7 +358,7 @@ namespace algebraic_numbers {
            return a.to_algebraic()->m_p_sz - 1;
        }

-        void swap(numeral & a, numeral & b) {
+        void swap(numeral & a, numeral & b) noexcept {
            std::swap(a.m_cell, b.m_cell);
        }

@ -2935,7 +2935,7 @@ namespace algebraic_numbers {
        return m_imp->to_rational(const_cast<numeral&>(a), r);
    }

-    void manager::swap(numeral & a, numeral & b) {
+    void manager::swap(numeral & a, numeral & b) noexcept {
        return m_imp->swap(a, b);
    }

--- a/src/math/polynomial/algebraic_numbers.h
+++ b/src/math/polynomial/algebraic_numbers.h
@ -129,7 +129,7 @@ namespace algebraic_numbers {
        void set(numeral & a, mpq const & n);
        void set(numeral & a, numeral const & n);

-        void swap(numeral & a, numeral & b);
+        void swap(numeral & a, numeral & b) noexcept;

        /**
           \brief Store in b an integer value smaller than 'a'.
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@ -447,7 +447,7 @@ namespace polynomial {
        }
    };

-    inline void swap(monomial * & m1, monomial * & m2) { std::swap(m1, m2); }
+    inline void swap(monomial * & m1, monomial * & m2) noexcept { std::swap(m1, m2); }

    typedef chashtable<monomial*, monomial::hash_proc, monomial::eq_proc> monomial_table;

--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@ -126,7 +126,7 @@ namespace upolynomial {
        m_factors[i].swap(p);
    }

-    void core_manager::factors::swap(factors & other) {
+    void core_manager::factors::swap(factors & other) noexcept {
        m_factors.swap(other.m_factors);
        m_degrees.swap(other.m_degrees);
        nm().swap(m_constant, other.m_constant);
--- a/src/math/polynomial/upolynomial.h
+++ b/src/math/polynomial/upolynomial.h
@ -89,7 +89,7 @@ namespace upolynomial {
            void push_back_swap(numeral_vector & p, unsigned degree);
            
            void swap_factor(unsigned i, numeral_vector & p);
-            void swap(factors & other);
+            void swap(factors & other) noexcept;
            void multiply(numeral_vector & out) const; 
            
            void display(std::ostream & out) const;
--- a/src/math/polynomial/upolynomial_factorization_int.h
+++ b/src/math/polynomial/upolynomial_factorization_int.h
@ -85,7 +85,7 @@ namespace upolynomial {

        unsigned max_degree() const { return m_set.size() - 1; }

-        void swap(factorization_degree_set & other) {
+        void swap(factorization_degree_set & other) noexcept {
            m_set.swap(other.m_set);
        }

--- a/src/math/realclosure/mpz_matrix.h
+++ b/src/math/realclosure/mpz_matrix.h
@ -50,7 +50,7 @@ public:
        SASSERT(j < n); 
        return a_ij[i*n + j]; }
    mpz & operator()(unsigned i, unsigned j) { SASSERT(i < m); SASSERT(j < n); return a_ij[i*n + j]; }
-    void swap(mpz_matrix & B) { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); }
+    void swap(mpz_matrix & B) noexcept { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); }
    mpz * row(unsigned i) const { SASSERT(i < m); return a_ij + i*n; }
 };

@ -136,7 +136,7 @@ public:
    mpz_matrix const & get() const { return A; }
    mpz_matrix & get() { return A; }

-    void swap(mpz_matrix & B) { A.swap(B); }
+    void swap(mpz_matrix & B) noexcept { A.swap(B); }

    void set(unsigned i, unsigned j, mpz const & v) { nm().set(A(i, j), v); }
    void set(unsigned i, unsigned j, int v) { nm().set(A(i, j), v); }
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@ -135,7 +135,7 @@ namespace realclosure {
    typedef interval_manager<mpbq_config> mpbqi_manager;
    typedef mpbqi_manager::interval       mpbqi;

-    void swap(mpbqi & a, mpbqi & b) {
+    void swap(mpbqi & a, mpbqi & b) noexcept {
        swap(a.m_lower, b.m_lower);
        swap(a.m_upper, b.m_upper);
        std::swap(a.m_lower_inf, b.m_lower_inf);
@ -2534,7 +2534,7 @@ namespace realclosure {
            return depends_on_infinitesimals(a.m_value);
        }

-        static void swap(mpbqi & a, mpbqi & b) {
+        static void swap(mpbqi & a, mpbqi & b) noexcept {
            realclosure::swap(a, b);
        }

@ -6313,7 +6313,7 @@ namespace realclosure {
        m_imp->set(a, n);
    }

-    void manager::swap(numeral & a, numeral & b) {
+    void manager::swap(numeral & a, numeral & b) noexcept {
        std::swap(a.m_value, b.m_value);
    }

--- a/src/math/realclosure/realclosure.h
+++ b/src/math/realclosure/realclosure.h
@ -164,7 +164,7 @@ namespace realclosure {
        void set(numeral & a, mpq const & n);
        void set(numeral & a, numeral const & n);

-        void swap(numeral & a, numeral & b);
+        void swap(numeral & a, numeral & b) noexcept;

        /**
           \brief Return a^{1/k}
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@ -484,7 +484,7 @@ namespace datalog {

            virtual bool can_swap(const base_object & o) const { return false; }

-            virtual void swap(base_object & o) {
+            virtual void swap(base_object & o) noexcept {
                std::swap(m_kind, o.m_kind);
 #if DL_LEAK_HUNTING
                m_leak_guard = get_plugin().get_ast_manager().mk_fresh_sort(get_plugin().get_name().bare_str());
@ -910,7 +910,7 @@ namespace datalog {
    public:
        table_signature() : m_functional_columns(0) {}

-        void swap(table_signature & s) {
+        void swap(table_signature & s) noexcept {
            signature_base::swap(s);
            std::swap(m_functional_columns, s.m_functional_columns);
        }
--- a/src/muz/rel/dl_finite_product_relation.cpp
+++ b/src/muz/rel/dl_finite_product_relation.cpp
@ -1835,7 +1835,7 @@ namespace datalog {
        }
    }

-    void finite_product_relation::swap(relation_base & r0) {
+    void finite_product_relation::swap(relation_base & r0) noexcept {
        SASSERT(can_swap(r0));
        finite_product_relation & r = finite_product_relation_plugin::get(r0);
        SASSERT(get_signature()==r.get_signature());
--- a/src/muz/rel/dl_finite_product_relation.h
+++ b/src/muz/rel/dl_finite_product_relation.h
@ -316,7 +316,7 @@ namespace datalog {

           Both relations must come from the same plugin and be of the same signature.
        */
-        void swap(relation_base & r) override;
+        void swap(relation_base & r) noexcept override;

        /**
           \brief Create a \c finite_product_relation object.
--- a/src/muz/rel/dl_vector_relation.h
+++ b/src/muz/rel/dl_vector_relation.h
@ -59,7 +59,7 @@ namespace datalog {
            dealloc(m_elems);
        }

-        void swap(relation_base& other) override {
+        void swap(relation_base& other) noexcept override {
            vector_relation& o = dynamic_cast<vector_relation&>(other);
            if (&o == this) return;
            std::swap(o.m_eqs, m_eqs);
--- a/src/nlsat/nlsat_assignment.h
+++ b/src/nlsat/nlsat_assignment.h
@ -33,7 +33,7 @@ namespace nlsat {
    public:
        assignment(anum_manager & _m):m_values(_m) {}
        anum_manager & am() const { return m_values.m(); }
-        void swap(assignment & other) {
+        void swap(assignment & other) noexcept {
            m_values.swap(other.m_values);
            m_assigned.swap(other.m_assigned);
        }
@ -67,7 +67,7 @@ namespace nlsat {
        anum_manager & m() const override { return am(); }
        bool contains(var x) const override { return is_assigned(x); }
        anum const & operator()(var x) const override { SASSERT(is_assigned(x)); return value(x); }
-        void swap(var x, var y) {
+        void swap(var x, var y) noexcept {
            SASSERT(x < m_values.size() && y < m_values.size());
            std::swap(m_assigned[x], m_assigned[y]);
            std::swap(m_values[x], m_values[y]);
--- a/src/nlsat/nlsat_scoped_literal_vector.h
+++ b/src/nlsat/nlsat_scoped_literal_vector.h
@ -67,7 +67,7 @@ namespace nlsat {
        void append(scoped_literal_vector const& ls) {
            append(ls.size(), ls.data());
        }
-        void swap(scoped_literal_vector& other) {
+        void swap(scoped_literal_vector& other) noexcept {
            SASSERT(&m_solver == &other.m_solver);
            m_lits.swap(other.m_lits);
        }
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@ -48,7 +48,7 @@ namespace nlsat {
    typedef chashtable<root_atom*, root_atom::hash_proc, root_atom::eq_proc> root_atom_table;

    // for apply_permutation procedure
-    void swap(clause * & c1, clause * & c2) {
+    void swap(clause * & c1, clause * & c2) noexcept {
        std::swap(c1, c2);
    }

--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@ -52,7 +52,7 @@ namespace opt {
        if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {            
            m_params.m_relevancy_lvl = 0;
        }
-        m_params.m_arith_auto_config_simplex = false;
+        m_params.m_arith_auto_config_simplex = true;
        m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads
        // m_params.m_auto_config = false;
    }
@ -67,7 +67,7 @@ namespace opt {
        m_dump_benchmarks = p.dump_benchmarks();
        m_params.updt_params(_p);
        m_context.updt_params(_p);
-        m_params.m_arith_auto_config_simplex = false;
+        m_params.m_arith_auto_config_simplex = true;
    }

    solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
--- a/src/sat/sat_cutset.h
+++ b/src/sat/sat_cutset.h
@ -183,7 +183,7 @@ namespace sat {
        void reset(on_update_t& on_del) { shrink(on_del, 0); }
        cut const & operator[](unsigned idx) const { return m_cuts[idx]; }
        void shrink(on_update_t& on_del, unsigned j); 
-        void swap(cut_set& other) { 
+        void swap(cut_set& other) noexcept {
            std::swap(m_var, other.m_var);
            std::swap(m_size, other.m_size); 
            std::swap(m_max_size, other.m_max_size); 
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@ -369,7 +369,7 @@ namespace sat {
        return result;
    }

-    void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) {
+    void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) noexcept {
        for (unsigned j = 0; j < sz; ++j) {
            if (v == clause[j].var()) {
                std::swap(clause[0], clause[j]);
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@ -91,7 +91,7 @@ namespace sat {

        bool legal_to_flip(bool_var v) const;

-        void swap(bool_var v, unsigned sz, literal_vector& clause);
+        void swap(bool_var v, unsigned sz, literal_vector& clause) noexcept;

        void add_elim_stack(entry & e);

--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@ -880,7 +880,6 @@ namespace sat {
        m_conflict = c;
        m_not_l    = not_l;
        TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
-        TRACE("sat", display_watches(tout));
    }

    void solver::assign_core(literal l, justification j) {
@ -1721,6 +1720,9 @@ namespace sat {
            if (next == null_bool_var)
                return false;
        }
+        else {
+            SASSERT(value(next) == l_undef);
+        }
        push();
        m_stats.m_decision++;
        
@ -1730,11 +1732,14 @@ namespace sat {
            phase = guess(next) ? l_true: l_false;
        
        literal next_lit(next, false);
+        SASSERT(value(next_lit) == l_undef);
        
        if (m_ext && m_ext->decide(next, phase)) {
+
            if (used_queue)
                m_case_split_queue.unassign_var_eh(next);
            next_lit = literal(next, false);
+            SASSERT(value(next_lit) == l_undef);
        }
                
        if (phase == l_undef)
@ -2430,9 +2435,8 @@ namespace sat {
        m_conflicts_since_restart++;
        m_conflicts_since_gc++;
        m_stats.m_conflict++;
-        if (m_step_size > m_config.m_step_size_min) {
-            m_step_size -= m_config.m_step_size_dec;
-        }
+        if (m_step_size > m_config.m_step_size_min)
+            m_step_size -= m_config.m_step_size_dec;        

        bool unique_max;
        m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        
@ -2555,7 +2559,8 @@ namespace sat {
                    }
                    SASSERT(lvl(c_var) < m_conflict_lvl);
                }
-                CTRACE("sat", idx == 0, 
+                CTRACE("sat", idx == 0,
+                       tout << "conflict level " << m_conflict_lvl << "\n";
                       for (literal lit : m_trail)
                           if (is_marked(lit.var()))
                               tout << "missed " << lit << "@" << lvl(lit) << "\n";);
@ -2810,8 +2815,9 @@ namespace sat {
        unsigned level = 0;

        if (not_l != null_literal) {
-            level = lvl(not_l);            
+            level = lvl(not_l);
        }      
+        TRACE("sat", tout << "level " << not_l << " is " << level << " " << js << "\n");

        switch (js.get_kind()) {
        case justification::NONE:
@ -3486,11 +3492,10 @@ namespace sat {
    //
    // -----------------------
    void solver::push() {
+        SASSERT(!m_ext || !m_ext->can_propagate());
        SASSERT(!inconsistent());
        TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
        SASSERT(m_qhead == m_trail.size());
-        if (m_ext) 
-            m_ext->unit_propagate();
        m_scopes.push_back(scope());
        scope & s = m_scopes.back();
        m_scope_lvl++;
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@ -5,6 +5,7 @@ z3_add_component(sat_smt
    arith_internalize.cpp
    arith_sls.cpp
    arith_solver.cpp
+    arith_value.cpp
    array_axioms.cpp
    array_diagnostics.cpp
    array_internalize.cpp
@ -28,6 +29,7 @@ z3_add_component(sat_smt
    euf_proof_checker.cpp
    euf_relevancy.cpp
    euf_solver.cpp
+    intblast_solver.cpp
    fpa_solver.cpp
    pb_card.cpp
    pb_constraint.cpp
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@ -205,6 +205,180 @@ namespace arith {
        add_clause(dgez, neg);
    }

+    bool solver::check_bv_term(app* n) {
+        unsigned sz;
+        expr* _x, * _y;
+        if (!ctx.is_relevant(expr2enode(n)))
+            return true;
+        expr_ref vx(m), vy(m),vn(m);
+        rational valn, valx, valy;
+        bool is_int;
+        VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
+        if (!get_value(expr2enode(_x), vx) || !get_value(expr2enode(_y), vy) || !get_value(expr2enode(n), vn)) {
+            IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
+            found_unsupported(n);
+            return true;
+        }
+        if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) {
+            IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
+            found_unsupported(n);
+            return true;
+        }
+        rational N = rational::power_of_two(sz);
+        valx = mod(valx, N);
+        valy = mod(valy, N);
+        expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
+        expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
+        SASSERT(0 <= valn && valn < N);
+        
+        // x mod 2^{i + 1} >= 2^i means the i'th bit is 1.
+        auto bitof = [&](expr* x, unsigned i) { 
+            expr_ref r(m);
+            r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i)));
+            return mk_literal(r);
+        };
+
+        if (a.is_band(n)) {
+            IF_VERBOSE(2, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n");
+            for (unsigned i = 0; i < sz; ++i) {
+                bool xb = valx.get_bit(i);
+                bool yb = valy.get_bit(i);
+                bool nb = valn.get_bit(i);
+                if (xb && yb && !nb)
+                    add_clause(~bitof(x, i), ~bitof(y, i), bitof(n, i));
+                else if (nb && !xb)
+                    add_clause(~bitof(n, i), bitof(x, i));
+                else if (nb && !yb)
+                    add_clause(~bitof(n, i), bitof(y, i));
+                else
+                    continue;
+                return false;
+            }
+        }
+        if (a.is_shl(n)) {
+            SASSERT(valy >= 0);
+            if (valy >= sz || valy == 0)
+                return true;
+            unsigned k = valy.get_unsigned();
+            rational r = mod(valx * rational::power_of_two(k), N);
+            if (r == valn)
+                return true;
+            sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)));
+            if (s().value(eq) == l_true)
+                return true;            
+            add_clause(~eq_internalize(y, a.mk_int(k)), eq);
+            IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
+            return false;
+        }
+        if (a.is_lshr(n)) {
+            SASSERT(valy >= 0);
+            if (valy >= sz || valy == 0)
+                return true;
+            unsigned k = valy.get_unsigned();
+            rational r = mod(div(valx, rational::power_of_two(k)), N);
+            if (r == valn)
+                return true;
+            sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))));
+            if (s().value(eq) == l_true)
+                return true;            
+            add_clause(~eq_internalize(y, a.mk_int(k)), eq);
+            IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
+            return false;
+        }
+        if (a.is_ashr(n)) {
+            SASSERT(valy >= 0);
+            if (valy >= sz || valy == 0)
+                return true;
+            unsigned k = valy.get_unsigned();
+            bool signvalx = x >= N/2;
+            rational valxdiv2k = div(valx, rational::power_of_two(k));
+            if (signvalx)
+                valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N);
+            if (valn == valxdiv2k)
+                return true;
+            sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
+            sat::literal eq;
+            expr* xdiv2k;
+            switch (s().value(signx)) {
+            case l_true:
+                // x < 0 & y = k -> n = (x div 2^k - 2^{N-k}) mod 2^N
+                xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
+                eq = eq_internalize(n, a.mk_mod(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), a.mk_int(N)));
+                if (s().value(eq) == l_true)
+                    return true;
+                break;
+            case l_false:
+                // x >= 0 & y = k -> n = x div 2^k
+                xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
+                eq = eq_internalize(n, xdiv2k);
+                if (s().value(eq) == l_true)
+                    return true;
+                break;
+            case l_undef:
+                ctx.mark_relevant(signx);
+                return false;
+            }
+            add_clause(~eq_internalize(y, a.mk_int(k)), ~signx, eq); 
+            return false;
+        }
+        return true;
+    }
+
+    bool solver::check_bv_terms() {
+        for (app* n : m_bv_terms) {
+            if (!check_bv_term(n)) {
+                ++m_stats.m_bv_axioms;
+                return false;
+            }
+        }
+        return true;
+    }
+
+    /*
+    * 0 <= x&y < 2^sz
+    * x&y <= x
+    * x&y <= y
+    */
+    void solver::mk_bv_axiom(app* n) {
+        unsigned sz;
+        expr* _x, * _y;
+        VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
+        rational N = rational::power_of_two(sz);
+        expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
+        expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
+
+        add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
+        add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
+
+        if (a.is_band(n)) {
+            add_clause(mk_literal(a.mk_le(n, x)));
+            add_clause(mk_literal(a.mk_le(n, y)));
+        }
+        else if (a.is_shl(n)) {
+            // y >= sz => n = 0
+            // y = 0 => n = x
+            add_clause(~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0))));
+            add_clause(~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
+        }
+        else if (a.is_lshr(n)) {
+            // y >= sz => n = 0
+            // y = 0 => n = x
+            add_clause(~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0))));
+            add_clause(~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
+        }
+        else if (a.is_ashr(n)) {
+            // y >= sz & x < 2^{sz-1} => n = 0
+            // y >= sz & x >= 2^{sz-1} => n = -1
+            // y = 0 => n = x
+            auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
+            add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0))));
+            add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1))));
+            add_clause(~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x)));            
+        }
+        else
+            UNREACHABLE();
+    }
+
    void solver::mk_bound_axioms(api_bound& b) {
        theory_var v = b.get_var();
        lp_api::bound_kind kind1 = b.get_bound_kind();
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@ -252,6 +252,12 @@ namespace arith {
                    st.to_ensure_var().push_back(n1);
                    st.to_ensure_var().push_back(n2);
                }
+                else if (a.is_band(n) || a.is_shl(n) || a.is_ashr(n) || a.is_lshr(n)) {
+                    m_bv_terms.push_back(to_app(n));
+                    ctx.push(push_back_vector(m_bv_terms));
+                    mk_bv_axiom(to_app(n));
+                    ensure_arg_vars(to_app(n));
+                }
                else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
                    found_unsupported(n);
                    ensure_arg_vars(to_app(n));
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@ -619,17 +619,17 @@ namespace arith {
        }
    }

-    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+    bool solver::get_value(euf::enode* n, expr_ref& value) {
        theory_var v = n->get_th_var(get_id());
        expr* o = n->get_expr();
-        expr_ref value(m);
+
        if (m.is_value(n->get_root()->get_expr())) {
            value = n->get_root()->get_expr();
        }
        else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
            anum const& an = nl_value(v, m_nla->tmp1());
            if (a.is_int(o) && !m_nla->am().is_int(an))
-                value = a.mk_numeral(rational::zero(), a.is_int(o));       
+                value = a.mk_numeral(rational::zero(), a.is_int(o));
            else
                value = a.mk_numeral(m_nla->am(), nl_value(v, m_nla->tmp1()), a.is_int(o));
        }
@ -637,24 +637,35 @@ namespace arith {
            rational r = get_value(v);
            TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
            SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m_not_handled != nullptr || m.limit().is_canceled()));
-            if (a.is_int(o) && !r.is_int()) 
+            if (a.is_int(o) && !r.is_int())
                r = floor(r);
            value = a.mk_numeral(r, o->get_sort());
        }
+        else
+            return false;
+
+        return true;
+    }
+
+
+    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+        expr_ref value(m);
+        expr* o = n->get_expr();
+        if (get_value(n, value))
+            ;
        else if (a.is_arith_expr(o) && reflect(o)) {
            expr_ref_vector args(m);
            for (auto* arg : *to_app(o)) {
                if (m.is_value(arg))
                    args.push_back(arg);
-                else 
+                else
                    args.push_back(values.get(ctx.get_enode(arg)->get_root_id()));
            }
            value = m.mk_app(to_app(o)->get_decl(), args.size(), args.data());
            ctx.get_rewriter()(value);
        }
-        else {
-            value = mdl.get_fresh_value(o->get_sort());
-        }
+        else
+            value = mdl.get_fresh_value(n->get_sort());
        mdl.register_value(value);
        values.set(n->get_root_id(), value);
    }
@ -1042,6 +1053,9 @@ namespace arith {
        if (!check_delayed_eqs()) 
            return sat::check_result::CR_CONTINUE;

+        if (!int_undef && !check_bv_terms())
+            return sat::check_result::CR_CONTINUE;
+
        if (ctx.get_config().m_arith_ignore_int && int_undef)
            return sat::check_result::CR_GIVEUP;
        if (m_not_handled != nullptr) {
@ -1192,7 +1206,8 @@ namespace arith {
            lia_check = l_undef;
            break;
        case lp::lia_move::continue_with_check:
-            lia_check = l_undef;
+            TRACE("arith", tout << "continue-with-check\n");
+            lia_check = l_false;
            break;
        default:
            UNREACHABLE();
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@ -214,6 +214,7 @@ namespace arith {
        expr* m_not_handled = nullptr;
        ptr_vector<app>        m_underspecified;
        ptr_vector<expr>       m_idiv_terms;
+        ptr_vector<app>        m_bv_terms;
        vector<ptr_vector<api_bound> > m_use_list;        // bounds where variables are used.

        // attributes for incremental version:
@ -317,6 +318,7 @@ namespace arith {
        void mk_bound_axioms(api_bound& b);
        void mk_bound_axiom(api_bound& b1, api_bound& b2);
        void mk_power0_axioms(app* t, app* n);
+        void mk_bv_axiom(app* n);
        void flush_bound_axioms();
        void add_farkas_clause(sat::literal l1, sat::literal l2);

@ -408,6 +410,8 @@ namespace arith {
        bool  check_delayed_eqs();
        lbool check_lia();
        lbool check_nla();
+        bool check_bv_terms();
+        bool check_bv_term(app* n);
        void add_lemmas();
        void propagate_nla();
        void add_equality(lpvar v, rational const& k, lp::explanation const& exp);
@ -522,6 +526,8 @@ namespace arith {
        bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed);
        void consume(rational const& v, lp::constraint_index j);
        bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const;
+
+        bool get_value(euf::enode* n, expr_ref& val);
    };


--- a/src/sat/smt/arith_value.cpp
+++ b/src/sat/smt/arith_value.cpp
@ -0,0 +1,145 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    smt_arith_value.cpp
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "sat/smt/arith_value.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+namespace arith {
+
+    arith_value::arith_value(euf::solver& s) :
+        s(s), m(s.get_manager()), a(m) {}
+
+    void arith_value::init() {
+        if (!as)
+            as = dynamic_cast<arith::solver*>(s.fid2solver(a.get_family_id()));
+    }
+
+    bool arith_value::get_value(expr* e, rational& val) {
+        auto n = s.get_enode(e);
+        expr_ref _val(m);
+        init();
+        return n && as->get_value(n, _val) && a.is_numeral(_val, val);
+    }
+
+#if 0
+    bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) {
+        if (!s.get_enode(e))
+            return false;
+        init();
+        is_strict = false;
+        bool found = false;
+        bool is_strict1;
+        rational lo1;
+        for (auto sib : euf::enode_class(s.get_enode(e))) {
+            if (!as->get_lower(sib, lo1, is_strict1))
+                continue;
+            if (!found || lo1 > lo || lo == lo1 && is_strict1)
+                lo = lo1, is_strict = is_strict1;
+            found = true;
+        }
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";);
+        return found;
+    }
+
+    bool arith_value::get_up_equiv(expr* e, rational& hi, bool& is_strict) {
+        if (!s.get_enode(e))
+            return false;
+        init();
+        is_strict = false;
+        bool found = false;
+        bool is_strict1;
+        rational hi1;
+        for (auto sib : euf::enode_class(s.get_enode(e))) {
+            if (!as->get_upper(sib, hi1, is_strict1))
+                continue;
+            if (!found || hi1 < hi || hi == hi1 && is_strict1)
+                hi = hi1, is_strict = is_strict1;
+            found = true;
+        }
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";);
+        return found;
+    }
+
+    bool arith_value::get_up(expr* e, rational& up, bool& is_strict) const {
+        init();
+        enode* n = s.get_enode(e);
+        is_strict = false;
+        return n && as->get_upper(n, up, is_strict);
+    }
+
+    bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) const {
+        init();
+        enode* n = s.get_enode(e);
+        is_strict = false;
+        return n && as->get_lower(n, lo, is_strict);
+    }
+
+#endif
+
+
+#if 0
+
+
+    bool arith_value::get_value_equiv(expr* e, rational& val) const {
+        if (!m_ctx->e_internalized(e)) return false;
+        expr_ref _val(m);
+        enode* next = m_ctx->get_enode(e), * n = next;
+        do {
+            e = next->get_expr();
+            if (m_tha && m_tha->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (m_thi && m_thi->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (m_thr && m_thr->get_value(next, val)) return true;
+            next = next->get_next();
+        } while (next != n);
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
+        return false;
+    }
+
+    expr_ref arith_value::get_lo(expr* e) const {
+        rational lo;
+        bool s = false;
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) {
+            return expr_ref(a.mk_numeral(lo, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_up(expr* e) const {
+        rational up;
+        bool s = false;
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) {
+            return expr_ref(a.mk_numeral(up, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_fixed(expr* e) const {
+        rational lo, up;
+        bool s = false;
+        if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) {
+            return expr_ref(a.mk_numeral(lo, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+#endif
+
+};
--- a/src/sat/smt/arith_value.h
+++ b/src/sat/smt/arith_value.h
@ -0,0 +1,52 @@
+
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    arith_value.h
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/arith_decl_plugin.h"
+
+namespace euf {
+    class solver;
+}
+namespace arith {
+
+    class solver;
+
+    class arith_value {
+        euf::solver& s;
+        ast_manager& m;
+        arith_util a;
+        solver* as = nullptr;
+        void init();
+    public:
+        arith_value(euf::solver& s);
+        bool get_value(expr* e, rational& value);
+
+#if 0
+        bool get_lo_equiv(expr* e, rational& lo, bool& strict);
+        bool get_up_equiv(expr* e, rational& up, bool& strict);
+        bool get_lo(expr* e, rational& lo, bool& strict);
+        bool get_up(expr* e, rational& up, bool& strict);
+        bool get_value_equiv(expr* e, rational& value);
+        expr_ref get_lo(expr* e);
+        expr_ref get_up(expr* e);
+        expr_ref get_fixed(expr* e);
+#endif
+    };
+};
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@ -400,7 +400,7 @@ namespace dt {
            return;
        }
        SASSERT(val == l_undef || (val == l_false && !d->m_constructor));
-        ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
+        ctx.push(set_vector_idx_trail(d->m_recognizers, c_idx));
        d->m_recognizers[c_idx] = recognizer;
        if (val == l_false)
            propagate_recognizer(v, recognizer);
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@ -106,7 +106,6 @@ namespace euf {
            attach_node(mk_enode(e, 0, nullptr));        
        return true;
    }
-
    bool solver::post_visit(expr* e, bool sign, bool root) {
        unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
        m_args.reset();
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@ -282,7 +282,7 @@ namespace euf {
    }

    void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
-        out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
+        out << "Failed to validate b" << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
        s().display(out);
        euf::enode_vector nodes;
        nodes.push_back(n);
@ -302,7 +302,7 @@ namespace euf {
            if (mval != sval) {
                if (r->bool_var() != sat::null_bool_var)
                    out << "b" << r->bool_var() << " ";
-                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << mval << "\n";
+                out << bpp(r) << " :=\nvalue obtained from model:  " << sval << "\nvalue of the root expression:  " << mval << "\n";
                continue;
            }
            if (!m.is_bool(val))
@ -310,7 +310,7 @@ namespace euf {
            auto bval = s().value(r->bool_var());
            bool tt = l_true == bval;
            if (tt != m.is_true(sval))
-                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << bval << "\n";
+                out << bpp(r) << " :=\nvalue according to model:  " << sval << "\nvalue of Boolean literal:  " << bval << "\n";
        }
        for (euf::enode* r : nodes)
            if (r)
@ -357,6 +357,7 @@ namespace euf {
            if (!tt && !mdl.is_true(e))
                continue;
            CTRACE("euf", first, display_validation_failure(tout, mdl, n););
+            CTRACE("euf", first, display(tout));
            IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
            (void)first;
            first = false;
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@ -21,6 +21,7 @@ Author:
 #include "sat/smt/sat_smt.h"
 #include "sat/smt/pb_solver.h"
 #include "sat/smt/bv_solver.h"
+#include "sat/smt/intblast_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/array_solver.h"
 #include "sat/smt/arith_solver.h"
@ -134,8 +135,16 @@ namespace euf {
        special_relations_util sp(m);
        if (pb.get_family_id() == fid)
            ext = alloc(pb::solver, *this, fid);
-        else if (bvu.get_family_id() == fid)
-            ext = alloc(bv::solver, *this, fid);
+        else if (bvu.get_family_id() == fid) {
+            if (get_config().m_bv_solver == 0)
+                ext = alloc(bv::solver, *this, fid);
+            else if (get_config().m_bv_solver == 1)
+                throw default_exception("polysat solver is not integrated");
+            else if (get_config().m_bv_solver == 2)
+                ext = alloc(intblast::solver, *this);
+            else 
+                throw default_exception("unknown bit-vector solver. Accepted values 0 (bit blast), 1 (polysat), 2 (int blast)");
+        }
        else if (au.get_family_id() == fid)
            ext = alloc(array::solver, *this, fid);
        else if (fpa.get_family_id() == fid)
@ -209,6 +218,15 @@ namespace euf {
        s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
    }

+    lbool solver::resolve_conflict() {
+        for (auto* s : m_solvers) {
+            lbool r = s->resolve_conflict();
+            if (r != l_undef)
+                return r;
+        }
+        return l_undef;
+    }
+
    /**
    Retrieve set of literals r that imply r.
    Since the set of literals are retrieved modulo multiple theories in a single implication
@ -281,6 +299,26 @@ namespace euf {
        }
    }

+    void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) {
+        m_egraph.begin_explain();
+        m_explain.reset();
+	m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
+	for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
+	    size_t* e = m_explain[qhead];
+	    if (is_literal(e)) 
+	        r.push_back(get_literal(e));            
+            else {
+                size_t idx = get_justification(e);
+                auto* ext = sat::constraint_base::to_extension(idx);
+                SASSERT(ext != this);
+                sat::literal lit = sat::null_literal;
+                ext->get_antecedents(lit, idx, r, true);
+            }
+        }
+        m_egraph.end_explain();
+    }
+
+
    void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {
        for (auto lit : euf::th_explain::lits(jst))
            r.push_back(lit);
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@ -363,11 +363,13 @@ namespace euf {
        bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); }
        size_t* to_justification(sat::literal l) { return to_ptr(l); }
        void set_conflict(th_explain* p) { set_conflict(p->to_index()); }
+        bool inconsistent() const { return s().inconsistent() || m_egraph.inconsistent(); }

        bool set_root(literal l, literal r) override;
        void flush_roots() override;

        void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
+        void get_eq_antecedents(enode* a, enode* b, literal_vector& r);
        void get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing);
        void add_eq_antecedent(bool probing, enode* a, enode* b);
        void explain_diseq(ptr_vector<size_t>& ex, cc_justification* cc, enode* a, enode* b);
@ -378,6 +380,7 @@ namespace euf {
        bool get_case_split(bool_var& var, lbool& phase) override;
        void asserted(literal l) override;
        sat::check_result check() override;
+        lbool resolve_conflict() override;
        void push() override;
        void pop(unsigned n) override;
        void user_push() override;
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@ -0,0 +1,145 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    intblast_solver.h
+
+Abstract:
+
+    Int-blast solver.
+
+    check_solver_state assumes a full assignment to literals in 
+    irredundant clauses. 
+    It picks a satisfying Boolean assignment and 
+    checks if it is feasible for bit-vectors using
+    an arithmetic solver.
+
+    The solver plugin is self-contained.
+
+    Internalize:
+    - internalize bit-vector terms bottom-up by updating m_translate.
+    - add axioms of the form:
+      - ule(b,a) <=> translate(ule(b, a))
+      - let arithmetic solver handle bit-vector constraints.
+    - For shared b
+      - Ensure: int2bv(translate(b)) = b
+      - but avoid bit-blasting by ensuring int2bv is injective (mod N) during final check
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2023-12-10
+
+--*/
+#pragma once
+
+#include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
+#include "solver/solver.h"
+#include "sat/smt/sat_th.h"
+#include "util/statistics.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace intblast {
+
+    class solver : public euf::th_euf_solver {
+        euf::solver& ctx;
+        sat::solver& s;
+        ast_manager& m;
+        bv_util bv;
+        arith_util a;
+        scoped_ptr<::solver> m_solver;
+        obj_map<func_decl, func_decl*> m_new_funs;
+        expr_ref_vector m_translate, m_args;
+        ast_ref_vector m_pinned;
+        sat::literal_vector m_core;
+        ptr_vector<app> m_bv2int, m_int2bv;
+        statistics m_stats;
+        bool m_is_plugin = true;        // when the solver is used as a plugin, then do not translate below quantifiers.        
+
+        bool is_bv(sat::literal lit);
+        void translate(expr_ref_vector& es);
+        void sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted);
+
+
+
+        bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
+        expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
+        void set_translated(expr* e, expr* r);
+        expr* arg(unsigned i) { return m_args.get(i); }
+
+        expr* umod(expr* bv_expr, unsigned i);
+        expr* smod(expr* bv_expr, unsigned i);
+        rational bv_size(expr* bv_expr);
+
+        void translate_expr(expr* e);
+        void translate_bv(app* e);
+        void translate_basic(app* e);
+        void translate_app(app* e);
+        void translate_quantifier(quantifier* q);
+        void translate_var(var* v);
+
+        void ensure_translated(expr* e);
+        void internalize_bv(app* e);
+
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
+        ptr_vector<expr> m_vars, m_preds;
+        bool add_bound_axioms();
+        bool add_predicate_axioms();
+
+        euf::theory_var mk_var(euf::enode* n) override;
+
+        void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
+        void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
+
+    public:
+        solver(euf::solver& ctx);
+        
+        ~solver() override {}
+
+        lbool check_solver_state();
+
+        sat::literal_vector const& unsat_core();
+
+        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
+
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+
+        void finalize_model(model& mdl) override;
+
+        std::ostream& display(std::ostream& out) const override;
+
+        void collect_statistics(statistics& st) const override;
+
+        bool unit_propagate() override;
+
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {}
+
+        sat::check_result check() override;
+
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out; }
+
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out; }
+
+        euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
+
+        void internalize(expr* e) override;
+
+        bool visited(expr* e) override;
+
+        bool post_visit(expr* e, bool sign, bool root) override;
+
+        bool visit(expr* e) override;
+
+        sat::literal internalize(expr* e, bool, bool) override;
+
+        void eq_internalized(euf::enode* n) override;
+
+        rational get_value(expr* e) const;
+
+    };
+
+}
--- a/src/sat/smt/pb_card.h
+++ b/src/sat/smt/pb_card.h
@ -33,7 +33,7 @@ namespace pb {
        literal const* begin() const { return m_lits; }
        literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
        void negate() override;
-        void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
+        void swap(unsigned i, unsigned j) noexcept override { std::swap(m_lits[i], m_lits[j]); }
        literal_vector literals() const override { return literal_vector(m_size, m_lits); }
        bool is_watching(literal l) const override;
        literal get_lit(unsigned i) const override { return m_lits[i]; }
--- a/src/sat/smt/pb_constraint.h
+++ b/src/sat/smt/pb_constraint.h
@ -102,7 +102,7 @@ namespace pb {
        
        virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
        virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
-        virtual void swap(unsigned i, unsigned j) { UNREACHABLE(); }
+        virtual void swap(unsigned i, unsigned j) noexcept { UNREACHABLE(); }
        virtual literal get_lit(unsigned i) const { UNREACHABLE(); return sat::null_literal; }
        virtual void set_lit(unsigned i, literal l) { UNREACHABLE(); }
        virtual void negate() { UNREACHABLE(); }
--- a/src/sat/smt/pb_pb.h
+++ b/src/sat/smt/pb_pb.h
@ -46,7 +46,7 @@ namespace pb {
        bool is_cardinality() const;
        void negate() override;
        void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
-        void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); }
+        void swap(unsigned i, unsigned j) noexcept override { std::swap(m_wlits[i], m_wlits[j]); }
        literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
        bool is_watching(literal l) const override;
        literal get_lit(unsigned i) const override { return m_wlits[i].second; }
--- a/src/smt/old_interval.cpp
+++ b/src/smt/old_interval.cpp
@ -238,7 +238,7 @@ interval & interval::operator=(interval const & other) {
    return *this;
 }

-interval & interval::operator=(interval && other) {
+interval & interval::operator=(interval && other) noexcept {
    SASSERT(&m_manager == &other.m_manager);
    m_lower = std::move(other.m_lower);
    m_upper = std::move(other.m_upper);
--- a/src/smt/old_interval.h
+++ b/src/smt/old_interval.h
@ -92,7 +92,7 @@ public:
    rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); }
    rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); }
    old_interval & operator=(old_interval const & other);
-    old_interval & operator=(old_interval && other);
+    old_interval & operator=(old_interval && other) noexcept;
    old_interval & operator+=(old_interval const & other);
    old_interval & operator-=(old_interval const & other);
    old_interval & operator*=(old_interval const & other);
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@ -55,6 +55,7 @@ def_module_params(module_name='smt',
                          ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
                          ('bv.polysat', BOOL, True, 'use polysat bit-vector solver'),
                          ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
+                          ('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
                          ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                          ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                          ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
--- a/src/smt/params/theory_bv_params.cpp
+++ b/src/smt/params/theory_bv_params.cpp
@ -29,6 +29,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
    m_bv_delay = p.bv_delay();
    m_bv_polysat = p.bv_polysat();
    m_bv_size_reduce = p.bv_size_reduce();
+    m_bv_solver = p.bv_solver();
 }

 #define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
@ -44,4 +45,5 @@ void theory_bv_params::display(std::ostream & out) const {
    DISPLAY_PARAM(m_bv_delay);
    DISPLAY_PARAM(m_bv_polysat);
    DISPLAY_PARAM(m_bv_size_reduce);
+    DISPLAY_PARAM(m_bv_solver);
 }
--- a/src/smt/params/theory_bv_params.h
+++ b/src/smt/params/theory_bv_params.h
@ -37,6 +37,7 @@ struct theory_bv_params {
    bool         m_bv_delay = true;
    bool         m_bv_polysat = false;
    bool         m_bv_size_reduce = false;
+    unsigned     m_bv_solver = 0;
    theory_bv_params(params_ref const & p = params_ref()) {
        updt_params(p);
    }
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@ -83,9 +83,11 @@ namespace smt {

    template<typename Ext>
    void theory_arith<Ext>::display_row(std::ostream & out, row const & r, bool compact) const {
-
+        if (static_cast<unsigned>(r.get_base_var()) >= m_columns.size())
+            return;
        column const & c   = m_columns[r.get_base_var()];
-        out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : ";
+        if (c.size() > 0)
+            out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : ";
        bool first = true;
        for (auto const& e : r) {
            if (!e.is_dead()) {
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@ -915,7 +915,7 @@ namespace smt {
            }
            SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
            d->m_recognizers[c_idx] = recognizer;
-            m_trail_stack.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
+            m_trail_stack.push(set_vector_idx_trail(d->m_recognizers, c_idx));
            if (val == l_false) {
                propagate_recognizer(v, recognizer);
            }
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@ -39,7 +39,7 @@ class simplifier_solver : public solver {
        bool m_updated = false;
        dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {}
        ~dep_expr_state() override {}
-        virtual unsigned qtail() const override { return s.m_fmls.size(); }
+        unsigned qtail() const override { return s.m_fmls.size(); }
        dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
        void update(unsigned i, dependent_expr const& j) override { 
            SASSERT(j.fml());  
--- a/src/util/array.h
+++ b/src/util/array.h
@ -184,7 +184,7 @@ public:
    T const * data() const { return m_data; }
    T * data() { return m_data; }

-    void swap(array & other) {
+    void swap(array & other) noexcept {
        std::swap(m_data, other.m_data);
    }

--- a/src/util/basic_interval.h
+++ b/src/util/basic_interval.h
@ -52,8 +52,8 @@ public:
        interval const & get() const { return m_interval; }
        interval & get() { return m_interval; }
        void reset() { m().reset(m_interval); }
-        void swap(scoped_interval & a) { m().swap(m_interval, a.m_interval); }
-        void swap(interval & a) { m().swap(m_interval, a); }
+        void swap(scoped_interval & a) noexcept { m().swap(m_interval, a.m_interval); }
+        void swap(interval & a) noexcept { m().swap(m_interval, a); }
        bound const & lower() const { return m_interval.lower(); }
        bound const & upper() const { return m_interval.upper(); }
        bound & lower() { return m_interval.lower(); }
@ -146,7 +146,7 @@ public:
        m().set(a.m_upper, n);
    }

-    void swap(interval & a, interval & b) {
+    void swap(interval & a, interval & b) noexcept {
        m().swap(a.m_lower, b.m_lower);
        m().swap(a.m_upper, b.m_upper);
    }
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@ -98,7 +98,7 @@ public:
        m_num_bits = 0;
    }

-    void swap(bit_vector & other) {
+    void swap(bit_vector & other) noexcept {
        std::swap(m_data, other.m_data);
        std::swap(m_num_bits, other.m_num_bits);
        std::swap(m_capacity, other.m_capacity);
--- a/src/util/chashtable.h
+++ b/src/util/chashtable.h
@ -553,7 +553,7 @@ public:
    iterator begin() const { return iterator(m_table, m_table + m_slots); }
    iterator end() const { return iterator(); }

-    void swap(chashtable & other) {
+    void swap(chashtable & other) noexcept {
        std::swap(m_table,       other.m_table);
        std::swap(m_capacity,    other.m_capacity);
        std::swap(m_init_slots,  other.m_init_slots);
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@ -223,6 +223,16 @@ public:
    }
 };

+template <typename T>
+class dll_elements {
+    T const* m_list;
+public:
+    dll_elements(T const* list) : m_list(list) {}
+    dll_iterator<T> begin() const { return dll_iterator<T>::mk_begin(m_list); }
+    dll_iterator<T> end() const { return dll_iterator<T>::mk_end(m_list); }
+};
+
+
 template < typename T
         , typename U = std::enable_if_t<std::is_base_of_v<dll_base<T>, T>>  // should only match if T actually inherits from dll_base<T>
         >
--- a/src/util/double_manager.h
+++ b/src/util/double_manager.h
@ -76,7 +76,7 @@ public:
    static void set(double & a, unsigned val) { a = static_cast<double>(val); }
    static void set(double & a, int64_t val) { a = static_cast<double>(val); }
    static void set(double & a, uint64_t val) { a = static_cast<double>(val); }
-    static void swap(double & a, double & b) { std::swap(a, b); }
+    static void swap(double & a, double & b) noexcept { std::swap(a, b); }
    bool is_pos(double a) const { return a > m_zero_tolerance; }
    bool is_neg(double a) const { return a < m_zero_tolerance; }
    bool is_zero(double a) const { return  -m_zero_tolerance <= a && a <= m_zero_tolerance; }
--- a/src/util/f2n.h
+++ b/src/util/f2n.h
@ -45,7 +45,7 @@ public:
        m_manager.set(m_one, ebits, sbits, 1);
    }

-    f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits),
+    f2n(f2n && other) noexcept : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits),
        m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {}

    ~f2n() { 
@ -86,7 +86,7 @@ public:
    void set(numeral & o, numeral const & x) { m().set(o, x); check(o); }
    void set(numeral & o, mpq const & x) { m().set(o, m_ebits, m_sbits, m_mode, x); check(o); }
    void reset(numeral & o) { m().reset(o, m_ebits, m_sbits); }
-    static void swap(numeral & x, numeral & y) { x.swap(y); }
+    static void swap(numeral & x, numeral & y) noexcept { x.swap(y); }
    
    void add(numeral const & x, numeral const & y, numeral & o) { m().add(m_mode, x, y, o); check(o); }
    void sub(numeral const & x, numeral const & y, numeral & o) { m().sub(m_mode, x, y, o); check(o); }
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@ -283,7 +283,7 @@ public:
        delete_table();
    }

-    void swap(core_hashtable & source) {
+    void swap(core_hashtable & source) noexcept {
        std::swap(m_table,       source.m_table);
        std::swap(m_capacity,    source.m_capacity);
        std::swap(m_size,        source.m_size);
--- a/src/util/heap.h
+++ b/src/util/heap.h
@ -259,7 +259,7 @@ public:
        return m_values.end(); 
    }

-    void swap(heap & other) {
+    void swap(heap & other) noexcept {
        if (this != &other) {
            CASSERT("heap", other.check_invariant());
            CASSERT("heap", check_invariant());
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@ -35,7 +35,7 @@ class hwf {
    }

 public:
-    void swap(hwf & other) { std::swap(value, other.value); }
+    void swap(hwf & other) noexcept { std::swap(value, other.value); }
 };


--- a/src/util/inf_eps_rational.h
+++ b/src/util/inf_eps_rational.h
@ -38,7 +38,7 @@ class inf_eps_rational {

    struct eq_proc { bool operator()(inf_eps_rational const& r1, inf_eps_rational const& r2) const { return r1 == r2; } };

-    void swap(inf_eps_rational & n) { 
+    void swap(inf_eps_rational & n) noexcept {
        m_infty.swap(n.m_infty);
        m_r.swap(n.m_r);
    }
--- a/src/util/inf_int_rational.h
+++ b/src/util/inf_int_rational.h
@ -43,7 +43,7 @@ class inf_int_rational {

    struct eq_proc { bool operator()(inf_int_rational const& r1, inf_int_rational const& r2) const { return r1 == r2; } };

-    void swap(inf_int_rational & n) { 
+    void swap(inf_int_rational & n) noexcept {
        m_first.swap(n.m_first);
        std::swap(m_second, n.m_second);
    }
--- a/src/util/inf_rational.h
+++ b/src/util/inf_rational.h
@ -44,7 +44,7 @@ class inf_rational {

    struct eq_proc { bool operator()(inf_rational const& r1, inf_rational const& r2) const { return r1 == r2; } };

-    void swap(inf_rational & n) { 
+    void swap(inf_rational & n) noexcept {
        m_first.swap(n.m_first);
        m_second.swap(n.m_second);
    }
--- a/src/util/inf_s_integer.h
+++ b/src/util/inf_s_integer.h
@ -37,7 +37,7 @@ class inf_s_integer {

    struct eq_proc { bool operator()(inf_s_integer const& r1, inf_s_integer const& r2) const { return r1 == r2; } };

-    void swap(inf_s_integer & n) { 
+    void swap(inf_s_integer & n) noexcept {
        std::swap(m_first, n.m_first);
        std::swap(m_second, n.m_second);
    }
--- a/src/util/map.h
+++ b/src/util/map.h
@ -184,7 +184,7 @@ public:

    unsigned long long get_num_collision() const { return m_table.get_num_collision(); }

-    void swap(table2map & other) {
+    void swap(table2map & other) noexcept {
        m_table.swap(other.m_table);
    }

--- a/src/util/mpbq.h
+++ b/src/util/mpbq.h
@ -40,10 +40,10 @@ public:
    mpbq(int v, unsigned k):m_num(v), m_k(k) {}
    mpz const & numerator() const { return m_num; }
    unsigned k() const { return m_k; }
-    void swap(mpbq & other) { m_num.swap(other.m_num); std::swap(m_k, other.m_k); }
+    void swap(mpbq & other) noexcept { m_num.swap(other.m_num); std::swap(m_k, other.m_k); }
 };

-inline void swap(mpbq & m1, mpbq & m2) { m1.swap(m2); }
+inline void swap(mpbq & m1, mpbq & m2) noexcept { m1.swap(m2); }

 typedef svector<mpbq> mpbq_vector;

@ -72,7 +72,7 @@ public:
    mpbq_manager(unsynch_mpz_manager & m);
    ~mpbq_manager();

-    static void swap(mpbq & a, mpbq & b) { a.swap(b); }
+    static void swap(mpbq & a, mpbq & b) noexcept { a.swap(b); }

    void del(mpbq & a) { m_manager.del(a.m_num); }
    void reset(mpbq & a) { m_manager.reset(a.m_num); a.m_k = 0; }
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@ -41,7 +41,7 @@ mpf::mpf(unsigned _ebits, unsigned _sbits):
    set(ebits, sbits);
 }

-void mpf::swap(mpf & other) {
+void mpf::swap(mpf & other) noexcept {
    unsigned tmp = ebits;
    ebits = other.ebits;
    other.ebits = tmp;
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@ -52,7 +52,7 @@ public:
    mpf & operator=(mpf const & other) = delete;
    unsigned get_ebits() const { return ebits; }
    unsigned get_sbits() const { return sbits; }
-    void swap(mpf & other);
+    void swap(mpf & other) noexcept;
 };

 class mpf_manager {
@ -87,7 +87,7 @@ public:
    void neg(mpf & o);
    void neg(mpf const & x, mpf & o);
    
-    void swap(mpf& a, mpf& b) { a.swap(b); }
+    void swap(mpf& a, mpf& b) noexcept { a.swap(b); }

    bool is_zero(mpf const & x);
    bool is_neg(mpf const & x);
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@ -44,14 +44,14 @@ public:
        m_exponent(0) {
    }
    
-    void swap(mpff & other) { 
+    void swap(mpff & other) noexcept {
        unsigned sign    = m_sign;    m_sign    = other.m_sign;    other.m_sign = sign;
        unsigned sig_idx = m_sig_idx; m_sig_idx = other.m_sig_idx; other.m_sig_idx = sig_idx;
        std::swap(m_exponent, other.m_exponent); 
    }
 };

-inline void swap(mpff & m1, mpff & m2) { m1.swap(m2); }
+inline void swap(mpff & m1, mpff & m2) noexcept { m1.swap(m2); }

 class mpz;
 class mpq;
@ -316,7 +316,7 @@ public:
    */
    static void abs(mpff & a) { a.m_sign = 0; }

-    static void swap(mpff & a, mpff & b) { a.swap(b); }
+    static void swap(mpff & a, mpff & b) noexcept { a.swap(b); }

    /**
       \brief c <- a + b
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@ -38,13 +38,13 @@ public:
        m_sig_idx(0) {
    }
    
-    void swap(mpfx & other) { 
+    void swap(mpfx & other) noexcept {
        unsigned sign    = m_sign;    m_sign    = other.m_sign;    other.m_sign = sign;
        unsigned sig_idx = m_sig_idx; m_sig_idx = other.m_sig_idx; other.m_sig_idx = sig_idx;
    }
 };

-inline void swap(mpfx & m1, mpfx & m2) { m1.swap(m2); }
+inline void swap(mpfx & m1, mpfx & m2) noexcept { m1.swap(m2); }

 class mpz;
 class mpq;
@ -228,7 +228,7 @@ public:
    */
    static void abs(mpfx & a) { a.m_sign = 0; }

-    static void swap(mpfx & a, mpfx & b) { a.swap(b); }
+    static void swap(mpfx & a, mpfx & b) noexcept { a.swap(b); }

    /**
       \brief c <- a + b
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@ -761,9 +761,9 @@ public:
        return temp;
    }

-    void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
+    void swap(mpz & a, mpz & b) noexcept { mpz_manager<SYNCH>::swap(a, b); }

-    void swap(mpq & a, mpq & b) {
+    void swap(mpq & a, mpq & b) noexcept {
        swap(a.m_num, b.m_num);
        swap(a.m_den, b.m_den);
    }
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@ -52,7 +52,7 @@ public:
        m.del(a.second);
    }

-    void swap(mpq_inf & a, mpq_inf & b) {
+    void swap(mpq_inf & a, mpq_inf & b) noexcept {
        m.swap(a.first, b.first);
        m.swap(a.second, b.second);
    }
--- a/Show more
+++ b/Show more