diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index db87cd008..9170effb4 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2108,6 +2108,7 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
 }
 
 br_status bv_rewriter::mk_bv_and(unsigned num, expr * const * args, expr_ref & result) {
+    return BR_FAILED;
     ptr_buffer<expr> new_args;
     for (unsigned i = 0; i < num; i++) {
         new_args.push_back(m_util.mk_bv_not(args[i]));
diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
index 8ab6be641..26eb5bc1b 100644
--- a/src/ast/simplifiers/extract_eqs.cpp
+++ b/src/ast/simplifiers/extract_eqs.cpp
@@ -20,6 +20,7 @@ Author:
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/simplifiers/extract_eqs.h"
 #include "ast/simplifiers/bound_manager.h"
 #include "params/tactic_params.hpp"
@@ -81,6 +82,76 @@ namespace euf {
         }
     };
 
+    class bv_extract_eq : public extract_eq {
+        ast_manager& m;
+        bv_util bv;
+        bool               m_enabled = true;
+
+        void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            if (!bv.is_bv_add(x))
+                return;
+
+            rational r, r_inverse;
+            unsigned i = 0;
+            expr_ref term(m);
+            expr* u, *z;
+            auto mk_term = [&](unsigned i) {
+                term = y;
+                unsigned j = 0;
+                for (expr* arg2 : *to_app(x)) {
+                    if (i != j)
+                        term = bv.mk_bv_sub(term, arg2);
+                    ++j;
+                }
+            };
+
+            unsigned sz;
+            for (expr* arg : *to_app(x)) {
+                if (is_uninterp_const(arg)) {
+                    mk_term(i);
+                    eqs.push_back(dependent_eq(orig, to_app(arg), term, d));
+                }
+                else if (bv.is_bv_mul(arg, u, z) && bv.is_numeral(u, r, sz) && is_uninterp_const(z) && r.is_odd()) {
+                    r.mult_inverse(sz, r_inverse);
+                    mk_term(i);                    
+                    term = bv.mk_bv_mul(bv.mk_numeral(r_inverse, sz), term);
+                    eqs.push_back(dependent_eq(orig, to_app(z), term, d));
+                }
+                ++i;
+            }
+                
+
+        }
+
+        void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            solve_add(orig, x, y, d, eqs);            
+        }
+
+    public:
+        bv_extract_eq(ast_manager& m): m(m), bv(m) {}
+
+        void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
+            if (!m_enabled)
+                return;
+            auto [f, p, d] = e();
+            expr* x, * y;
+            if (m.is_eq(f, x, y) && bv.is_bv(x)) {
+                solve_eq(f, x, y, d, eqs);
+                solve_eq(f, y, x, d, eqs);
+            }
+        }
+
+        void pre_process(dependent_expr_state& fmls) override {
+        }
+
+
+        void updt_params(params_ref const& p) override {
+            tactic_params tp(p);
+            m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver());
+        }
+
+    };
+
     class arith_extract_eq : public extract_eq {
         ast_manager&       m;
         arith_util         a;
@@ -254,7 +325,7 @@ break;
             }
         }
 
-        void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+         void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
             solve_add(orig, x, y, d, eqs);
             solve_mod(orig, x, y, d, eqs);
             solve_mul(orig, x, y, d, eqs);
@@ -311,5 +382,6 @@ break;
     void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex) {
         ex.push_back(alloc(arith_extract_eq, m));
         ex.push_back(alloc(basic_extract_eq, m));
+        ex.push_back(alloc(bv_extract_eq, m));
     }
 }
diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index f510979e8..e9833bc19 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -212,9 +212,11 @@ namespace polysat {
     sat::check_result core::check() {
         lbool r = l_true;
 
+        verbose_stream() << "check-propagate\n";
         if (propagate())
             return sat::check_result::CR_CONTINUE;
 
+        verbose_stream() << "check-assign-variable\n";
         switch (assign_variable()) {
         case l_true:
             break;
@@ -228,6 +230,7 @@ namespace polysat {
             break;
         }
 
+        verbose_stream() << "check-saturate\n";
         saturation saturate(*this);
         switch (saturate()) {
         case l_true:
@@ -240,7 +243,8 @@ namespace polysat {
             r = l_undef;
             break;
         }
-
+        
+        verbose_stream() << "check-refine\n";
         switch (m_monomials.refine()) {
         case l_true:
             break;
@@ -253,6 +257,7 @@ namespace polysat {
             break;
         }
 
+        verbose_stream() << "check-blast\n";
         switch (m_monomials.bit_blast()) {
         case l_true:
             break;
diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp
index 8d788c530..c6022fadd 100644
--- a/src/sat/smt/polysat/op_constraint.cpp
+++ b/src/sat/smt/polysat/op_constraint.cpp
@@ -456,6 +456,8 @@ namespace polysat {
         auto rv = c.subst(r);
         auto& C = c.cs();
 
+        verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n";
+
         if (!pv.is_val() || !qv.is_val() || !rv.is_val())
             return false;
 
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 69be7c22f..6c77bb657 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -359,7 +359,9 @@ namespace polysat {
         if (a.degree(v) < r.degree(v))
             return;
 
+        verbose_stream() << "resolve: " << a << " = " << b << " => " << r << "\n";
         add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);
+        exit(0);
     }
 
 
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 219ffa733..1ba409c92 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -868,7 +868,7 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[  src ~4 <= 43691*v0;
             }
         }
 
-        IF_VERBOSE(1, {
+        IF_VERBOSE(3, {
             for (auto const& e : m_explain)
                 if (e.mark)
                     display_explain(verbose_stream() << "redundant: ", e) << "\n";
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 082af36d8..235dbafd6 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -18,6 +18,7 @@ Author:
 #include "params/bv_rewriter_params.hpp"
 #include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
+#include "ast/rewriter/bit_blaster/bit_blaster.h"
 
 namespace polysat {
 
@@ -159,7 +160,9 @@ namespace polysat {
             m_delayed_axioms.push_back(a);
             ctx.push(push_back_vector(m_delayed_axioms));
             break;
-
+        case OP_BIT2BOOL:
+            internalize_bit2bool(a);
+            break;
         default:
             IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
             NOT_IMPLEMENTED_YET();
@@ -286,6 +289,16 @@ namespace polysat {
         m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n));
     }
 
+    void solver::internalize_bit2bool(app* n) {
+        expr* b = nullptr;
+        unsigned idx;
+        VERIFY(bv.is_bit2bool(n, b, idx));
+        pdd p = expr2pdd(b);
+        auto sc = m_core.bit(p, idx);
+        add_axiom("bit2bool", { eq_internalize(n, constraint2expr(sc)) });
+    }
+
+
     bool solver::propagate_delayed_axioms() {
         if (m_delayed_axioms_qhead == m_delayed_axioms.size())
             return false;
@@ -687,7 +700,7 @@ namespace polysat {
 
     void solver::internalize_mul(app* a) {
         vector<dd::pdd> args;
-        for (expr* arg : *to_app(a))
+        for (expr* arg : *a)
             args.push_back(expr2pdd(arg));
         if (args.size() == 1) {
             internalize_set(a, args[0]);
@@ -701,6 +714,29 @@ namespace polysat {
             internalize_set(a, args[0] * args[1]);
             return;
         }
+
+#if 0
+        // experiment with eagerly bit-blasting multiplication.
+        if (args.size() == 2) {
+            unsigned sz = bv.get_bv_size(a);
+            expr_ref_vector xs(m), ys(m), zs(m);
+            for (unsigned i = 0; i < sz; ++i) {
+                xs.push_back(bv.mk_bit2bool(a->get_arg(0), i));
+                ys.push_back(bv.mk_bit2bool(a->get_arg(1), i));
+            }
+            bit_blaster_params p;
+            bit_blaster bb(m, p);
+            bb.mk_multiplier(xs.size(), xs.data(), ys.data(), zs);
+            pdd z = expr2pdd(a);
+            for (unsigned i = 0; i < sz; ++i) {
+                //                sat::literal bit_i = ctx.internalize(zs.get(i), false, false);
+                auto sc = m_core.bit(z, i);
+                add_axiom("mul", { eq_internalize(constraint2expr(sc), zs.get(i)) });
+            }
+            return;
+        }
+#endif
+        
         auto pv = m_core.mul(args.size(), args.data());
         m_pddvar2var.setx(pv, get_th_var(a), UINT_MAX);
         internalize_set(a, m_core.var(pv));