diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 2d4b9847e..b6606d4f6 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -135,11 +135,8 @@ 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);
-            dealloc(ext);
-            ext = alloc(polysat::solver, *this, fid);
-        }
+        else if (bvu.get_family_id() == fid) 
+            ext = alloc(polysat::solver, *this, fid);        
         else if (au.get_family_id() == fid)
             ext = alloc(array::solver, *this, fid);
         else if (fpa.get_family_id() == fid)
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 25ec308d8..239bb4682 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -79,6 +79,8 @@ namespace intblast {
         }
 
         m_core.reset();
+        m_vars.reset();
+        m_trail.reset();
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
         expr_ref_vector es(m);
@@ -89,12 +91,19 @@ namespace intblast {
 
         for (auto const& [src, vi] : m_vars) {
             auto const& [v, b] = vi;
+            verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n";
             m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
             m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
         }
+
+        verbose_stream() << "check\n";
+        m_solver->display(verbose_stream());
+        verbose_stream() << es << "\n";
                
         lbool r = m_solver->check_sat(es);
 
+        verbose_stream() << "result " << r << "\n";
+
         if (r == l_false) {
             expr_ref_vector core(m);
             m_solver->get_unsat_core(core);
@@ -114,8 +123,6 @@ namespace intblast {
             return false;
         if (m.is_and(e) || m.is_or(e) || m.is_not(e) || m.is_implies(e) || m.is_iff(e))
             return false;
-        if (is_quantifier(e))
-            return false;
         return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); });
     }
 
@@ -145,22 +152,34 @@ namespace intblast {
                 }
             }
         }
+        std::stable_sort(sorted.begin(), sorted.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
     }
 
     void solver::translate(expr_ref_vector& es) {
         ptr_vector<expr> todo;
         obj_map<expr, expr*> translated;        
         expr_ref_vector args(m);
-        m_trail.reset();
-        m_vars.reset();
         
         sorted_subterms(es, todo);
-        for (unsigned i = todo.size(); i-- > 0; ) {
-            expr* e = todo[i];
+        for (expr* e : todo) {
             if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
                 expr* b = q->get_expr();
-                m_trail.push_back(m.update_quantifier(q, translated[b]));
+
+                unsigned nd = q->get_num_decls();
+                ptr_vector<sort> sorts;
+                for (unsigned i = 0; i < nd; ++i) {
+                    auto s = q->get_decl_sort(i);
+                    if (bv.is_bv_sort(s)) {
+                        NOT_IMPLEMENTED_YET();
+                        sorts.push_back(a.mk_int());
+                    }
+                    else
+                        sorts.push_back(s);
+                }
+                b = translated[b];
+                // TODO if sorts contain integer, then created bounds variables.
+                m_trail.push_back(m.update_quantifier(q, b));
                 translated.insert(e, m_trail.back());
                 continue;
             }
@@ -177,11 +196,12 @@ namespace intblast {
                 continue;
             }
             app* ap = to_app(e);
+            expr* bv_expr = e;
             args.reset();
             for (auto arg : *ap)
                 args.push_back(translated[arg]);
 
-            auto bv_size = [&]() { return rational::power_of_two(bv.get_bv_size(e->get_sort())); };
+            auto bv_size = [&]() { return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort())); };
 
             auto mk_mod = [&](expr* x) {
                 if (m_vars.contains(x))
@@ -197,6 +217,7 @@ namespace intblast {
             if (m.is_eq(e)) {
                 bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); });
                 if (has_bv_arg) {
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(m.mk_eq(mk_mod(args.get(0)), mk_mod(args.get(1))));
                     translated.insert(e, m_trail.back());
                 }
@@ -229,6 +250,8 @@ namespace intblast {
                 m_trail.push_back(m.mk_app(f, args));
                 translated.insert(e, m_trail.back());
 
+                verbose_stream() << "translate " << mk_pp(e, m) << " " << has_bv_sort << "\n";
+
                 if (has_bv_sort) 
                     m_vars.insert(e, { m_trail.back(), bv_size() });
                 
@@ -272,6 +295,53 @@ namespace intblast {
                 case OP_BNEG:
                     m_trail.push_back(a.mk_uminus(args.get(0)));
                     break;
+                case OP_CONCAT: {
+                    expr_ref r(a.mk_int(0), m);
+                    unsigned sz = 0;
+                    for (unsigned i = 0; i < args.size(); ++i) {
+                        expr* old_arg = ap->get_arg(i);
+                        expr* new_arg = args.get(i);
+                        bv_expr = old_arg;
+                        new_arg = mk_mod(new_arg);
+                        if (sz > 0) {
+                            new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz)));
+                            r = a.mk_add(r, new_arg);
+                        }
+                        else 
+                            r = new_arg;                        
+                        sz += bv.get_bv_size(old_arg->get_sort());
+                    }
+                    m_trail.push_back(r);
+                    break;
+                }
+                case OP_EXTRACT: {
+                    unsigned lo, hi;
+                    expr* old_arg;
+                    VERIFY(bv.is_extract(e, lo, hi, old_arg));
+                    unsigned sz = hi - lo + 1;
+                    expr* new_arg = args.get(0);
+                    if (lo > 0)
+                        new_arg = a.mk_div(new_arg, a.mk_int(rational::power_of_two(lo)));
+                    m_trail.push_back(new_arg);
+                    break;
+                }   
+                case OP_BV_NUM: {
+                    rational val;
+                    unsigned sz;
+                    VERIFY(bv.is_numeral(e, val, sz));
+                    m_trail.push_back(a.mk_int(val));
+                    break;
+                }
+                case OP_BUREM_I: {
+                    expr* x = args.get(0), * y = args.get(1);
+                    m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, y)));
+                    break;
+                }
+                case OP_BUDIV_I: {
+                    expr* x = args.get(0), * y = args.get(1);
+                    m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y)));
+                    break;
+                }
                 case OP_BNOT:
                 case OP_BNAND:
                 case OP_BNOR:
@@ -296,9 +366,14 @@ namespace intblast {
                 case OP_BSREM:
                 case OP_BSMOD:
                 case OP_BAND:
+                    verbose_stream() << mk_pp(e, m) << "\n";
                     NOT_IMPLEMENTED_YET();
                     break;
+                default:
+                    verbose_stream() << mk_pp(e, m) << "\n";
+                    NOT_IMPLEMENTED_YET();
             }
+            verbose_stream() << "insert " << mk_pp(e, m) << " -> " << mk_pp(m_trail.back(), m) << "\n";
             translated.insert(e, m_trail.back());
         }
         for (unsigned i = 0; i < es.size(); ++i) 
diff --git a/src/sat/smt/polysat/polysat_constraints.cpp b/src/sat/smt/polysat/polysat_constraints.cpp
index 99da7b0db..faeea62a4 100644
--- a/src/sat/smt/polysat/polysat_constraints.cpp
+++ b/src/sat/smt/polysat/polysat_constraints.cpp
@@ -1,4 +1,4 @@
-/*++
+/*++
 Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
@@ -12,6 +12,7 @@ Author:
 
 --*/
 
+#include "util/log.h"
 #include "sat/smt/polysat/polysat_core.h"
 #include "sat/smt/polysat/polysat_constraints.h"
 #include "sat/smt/polysat/polysat_ule.h"
@@ -23,16 +24,34 @@ namespace polysat {
         pdd lhs = p, rhs = q;
         bool is_positive = true;
         ule_constraint::simplify(is_positive, lhs, rhs);
-        auto* c = alloc(ule_constraint, p, q);
-        m_trail.push(new_obj_trail(c));
-        auto sc = signed_constraint(ckind_t::ule_t, c);
+        auto* cnstr = alloc(ule_constraint, p, q);
+        c.trail().push(new_obj_trail(cnstr));
+        auto sc = signed_constraint(ckind_t::ule_t, cnstr);
         return is_positive ? sc : ~sc;
     }
 
     signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) { 
-        auto* c = alloc(umul_ovfl_constraint, p, q);
-        m_trail.push(new_obj_trail(c));
-        return signed_constraint(ckind_t::umul_ovfl_t, c);
+        auto* cnstr = alloc(umul_ovfl_constraint, p, q);
+        c.trail().push(new_obj_trail(cnstr));
+        return signed_constraint(ckind_t::umul_ovfl_t, cnstr);
+    }
+
+    bool signed_constraint::is_eq(pvar& v, rational& val) {
+        if (m_sign)
+            return false;
+        if (!is_ule())
+            return false;
+        auto const& ule = to_ule();
+        auto const& l = ule.lhs(), &r = ule.rhs();
+        if (!r.is_zero())
+            return false;
+        if (!l.is_unilinear())
+            return false;
+        if (!l.hi().is_one())
+            return false;
+        v = l.var();
+        val = -l.lo().val();
+        return true;
     }
 
     lbool signed_constraint::eval(assignment& a) const {
@@ -44,4 +63,11 @@ namespace polysat {
         if (m_sign) out << "~";
         return out << *m_constraint;        
     }
+
+    bool signed_constraint::is_always_true() const {
+        return m_sign ? m_constraint->is_always_false() : m_constraint->is_always_true();
+    }
+    bool signed_constraint::is_always_false() const {
+        return m_sign ? m_constraint->is_always_true() : m_constraint->is_always_false();
+    }
 }
diff --git a/src/sat/smt/polysat/polysat_constraints.h b/src/sat/smt/polysat/polysat_constraints.h
index 687b3d91a..fdef902e2 100644
--- a/src/sat/smt/polysat/polysat_constraints.h
+++ b/src/sat/smt/polysat/polysat_constraints.h
@@ -41,6 +41,8 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual lbool eval() const = 0;
         virtual lbool eval(assignment const& a) const = 0;
+        virtual bool is_always_true() const = 0;
+        virtual bool is_always_false() const = 0;
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@@ -61,6 +63,8 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_constraint->vars(); }
         unsigned var(unsigned idx) const { return m_constraint->var(idx); }
         bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
+        bool is_always_true() const;
+        bool is_always_false() const;
         lbool eval(assignment& a) const;
         ckind_t op() const { return m_op; }
         bool is_ule() const { return m_op == ule_t; }
@@ -68,27 +72,27 @@ namespace polysat {
         bool is_smul_fl() const { return m_op == smul_fl_t; }
         ule_constraint const& to_ule() const { return *reinterpret_cast<ule_constraint*>(m_constraint); }
         umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
-        bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
+        bool is_eq(pvar& v, rational& val);
         std::ostream& display(std::ostream& out) const;
     };
 
     inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); }
 
     class constraints {
-        trail_stack& m_trail;
+        core& c;
     public:
-        constraints(trail_stack& c) : m_trail(c) {}
+        constraints(core& c) : c(c) {}
 
         signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); }
         signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); }
         signed_constraint ule(pdd const& p, pdd const& q);
-        signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
-        signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
-        signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint sle(pdd const& p, pdd const& q) { auto sh = rational::power_of_two(p.power_of_2() - 1); return ule(p + sh, q + sh); }
+        signed_constraint ult(pdd const& p, pdd const& q) { return ~ule(q, p); }
+        signed_constraint slt(pdd const& p, pdd const& q) { return ~sle(q, p); }
         signed_constraint umul_ovfl(pdd const& p, pdd const& q);
-        signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
-        signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
-        signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); }
+        signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("smul ovfl nyi"); }
+        signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("smult-udfl nyi"); }
+        signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("bit nyi"); }
 
         signed_constraint diseq(pdd const& p) { return ~eq(p); }
         signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
@@ -138,4 +142,4 @@ namespace polysat {
         //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
         //signed_constraint odd(pdd const& p) { return ~even(p); }
     };
-}
\ No newline at end of file
+}
diff --git a/src/sat/smt/polysat/polysat_core.cpp b/src/sat/smt/polysat/polysat_core.cpp
index be25c9af8..f2bb995d7 100644
--- a/src/sat/smt/polysat/polysat_core.cpp
+++ b/src/sat/smt/polysat/polysat_core.cpp
@@ -80,7 +80,7 @@ namespace polysat {
     core::core(solver_interface& s) :
         s(s),         
         m_viable(*this),
-        m_constraints(s.trail()),
+        m_constraints(*this),
         m_assignment(*this),
         m_var_queue(m_activity)
     {}
diff --git a/src/sat/smt/polysat/polysat_core.h b/src/sat/smt/polysat/polysat_core.h
index 144b1256b..5262f2bbe 100644
--- a/src/sat/smt/polysat/polysat_core.h
+++ b/src/sat/smt/polysat/polysat_core.h
@@ -84,7 +84,8 @@ namespace polysat {
         void get_bitvector_prefixes(pvar v, pvar_vector& out);
         void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits);
         bool inconsistent() const;
-        
+        void add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
+
 
         void add_watch(unsigned idx, unsigned var);
 
@@ -114,29 +115,28 @@ namespace polysat {
         signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
 
 
-        pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd shl(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd band(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bor(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); }
-        pdd bnot(pdd a) { throw default_exception("nyi"); }
-        std::pair<pdd, pdd> quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); }
-        pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
-        pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
-        pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); }
-        pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); }
+        pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("lshr nyi"); }
+        pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("ashr nyi"); }
+        pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("shlh nyi"); }
+        pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("band nyi"); }
+        pdd bxor(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("bxor nyi"); }
+        pdd bor(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("bir ==nyi"); }
+        pdd bnand(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("bnand nyi"); }
+        pdd bxnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("bxnor nyi"); }
+        pdd bnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("bnotr nyi"); }
+        pdd bnot(pdd a) { NOT_IMPLEMENTED_YET();  throw default_exception("bnot nyi"); }
+        pdd zero_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET();  throw default_exception("zero ext nyi"); }
+        pdd sign_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET();  throw default_exception("sign ext nyi"); }
+        pdd extract(pdd src, unsigned hi, unsigned lo) { NOT_IMPLEMENTED_YET();  throw default_exception("extract nyi"); }
+        pdd concat(unsigned n, pdd const* args) { NOT_IMPLEMENTED_YET();  throw default_exception("concat nyi"); }
         pvar add_var(unsigned sz);
         pdd var(pvar p) { return m_vars[p]; }
-        unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
+        unsigned size(pvar v) const { return m_vars[v].power_of_2(); }
 
         constraints& cs() { return m_constraints; }
         trail_stack& trail();
 
-        std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
+        std::ostream& display(std::ostream& out) const { NOT_IMPLEMENTED_YET();  throw default_exception("nyi"); }
     };
 
 }
diff --git a/src/sat/smt/polysat/polysat_ule.cpp b/src/sat/smt/polysat/polysat_ule.cpp
index 0fb01bcae..7482ec36a 100644
--- a/src/sat/smt/polysat/polysat_ule.cpp
+++ b/src/sat/smt/polysat/polysat_ule.cpp
@@ -343,4 +343,22 @@ namespace polysat {
         return eval(a.apply_to(lhs()), a.apply_to(rhs()));
     }
 
+    bool ule_constraint::is_always_true() const {
+        if (lhs().is_zero())
+            return true;      // 0 <= p
+        if (rhs().is_max())
+            return true;      // p <= -1
+        if (lhs().is_val() && rhs().is_val())
+            return lhs().val() <= rhs().val();
+        return false;
+    }
+
+    bool ule_constraint::is_always_false() const {
+        if (lhs().is_never_zero() && rhs().is_zero())
+            return true;      // p > 0, q = 0
+        if (lhs().is_val() && rhs().is_val())
+            return lhs().val() > rhs().val();
+        return false;
+    }
+
 }
diff --git a/src/sat/smt/polysat/polysat_ule.h b/src/sat/smt/polysat/polysat_ule.h
index e21ed1029..2944bf614 100644
--- a/src/sat/smt/polysat/polysat_ule.h
+++ b/src/sat/smt/polysat/polysat_ule.h
@@ -35,6 +35,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
         lbool eval(assignment const& a) const override;
+        bool is_always_true() const override;
+        bool is_always_false() const override;
         bool is_eq() const { return m_rhs.is_zero(); }
         unsigned power_of_2() const { return m_lhs.power_of_2(); }
 
diff --git a/src/sat/smt/polysat/polysat_umul_ovfl.h b/src/sat/smt/polysat/polysat_umul_ovfl.h
index 41972ef59..65a12c031 100644
--- a/src/sat/smt/polysat/polysat_umul_ovfl.h
+++ b/src/sat/smt/polysat/polysat_umul_ovfl.h
@@ -34,6 +34,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
         lbool eval(assignment const& a) const override;
+        bool is_always_true() const override { return false; } // todo port
+        bool is_always_false() const override { return false; }
     };
 
 }
diff --git a/src/sat/smt/polysat/polysat_viable.cpp b/src/sat/smt/polysat/polysat_viable.cpp
index 4152956de..35158b889 100644
--- a/src/sat/smt/polysat/polysat_viable.cpp
+++ b/src/sat/smt/polysat/polysat_viable.cpp
@@ -90,6 +90,8 @@ namespace polysat {
     }
 
     lbool viable::find_viable(pvar v, rational& lo, rational& hi) {
+        return l_undef;
+
         fixed_bits_info fbi;
 
 #if 0
@@ -1007,7 +1009,7 @@ namespace polysat {
     }
 
     void viable::log(pvar v) {
-        throw default_exception("nyi");
+      // 
     }
 
 
diff --git a/src/sat/smt/polysat/polysat_viable.h b/src/sat/smt/polysat/polysat_viable.h
index f426dc326..88070a553 100644
--- a/src/sat/smt/polysat/polysat_viable.h
+++ b/src/sat/smt/polysat/polysat_viable.h
@@ -186,36 +186,36 @@ namespace polysat {
 
         template <bool FORWARD>
         bool refine_viable(pvar v, rational const& val, fixed_bits_info const& fbi) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         bool refine_viable(pvar v, rational const& val) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         template <bool FORWARD>
         bool refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         template <bool FORWARD>
         entry* refine_bits(pvar v, rational const& val, unsigned num_bits, fixed_bits_info const& fbi) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         bool refine_equal_lin(pvar v, rational const& val) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         bool refine_disequal_lin(pvar v, rational const& val) {
-            throw default_exception("nyi");
+            throw default_exception("refine nyi");
         }
 
         void set_conflict_by_interval(pvar v, unsigned w, ptr_vector<entry>& intervals, unsigned first_interval);
         bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, bool& create_lemma, uint_set& vars_to_explain);
 
         std::pair<entry*, bool> find_value(rational const& val, entry* entries) {
-            throw default_exception("nyi");
+            throw default_exception("fine_value nyi");
         }
 
         bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi);
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 95979348d..96f7def0e 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -1,4 +1,4 @@
-/*++
+/*++
 Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
@@ -22,7 +22,9 @@ Author:
 namespace polysat {
 
     euf::theory_var solver::mk_var(euf::enode* n) {
-        return euf::th_euf_solver::mk_var(n);
+        theory_var v = euf::th_euf_solver::mk_var(n);
+        ctx.attach_th_var(n, this, v);
+        return v;
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root) {
@@ -115,12 +117,13 @@ namespace polysat {
         case OP_BSADD_OVFL:
         case OP_BUSUB_OVFL:
         case OP_BSSUB_OVFL:
+            verbose_stream() << mk_pp(a, m) << "\n";
             // handled by bv_rewriter for now
             UNREACHABLE();
             break;
 
-        case OP_BUDIV_I:          internalize_div_rem_i(a, true); break;
-        case OP_BUREM_I:          internalize_div_rem_i(a, false); break;
+        case OP_BUDIV_I:          internalize_udiv_i(a); break;
+        case OP_BUREM_I:          internalize_urem_i(a); break;
 
         case OP_BUDIV:            internalize_div_rem(a, true); break;
         case OP_BUREM:            internalize_div_rem(a, false); break;
@@ -187,17 +190,93 @@ namespace polysat {
         mk_atom(lit.var(), sc);
     }
 
-    void solver::internalize_div_rem_i(app* e, bool is_div) {
-        auto p = expr2pdd(e->get_arg(0));
-        auto q = expr2pdd(e->get_arg(1));
-        auto [quot, rem] = m_core.quot_rem(p, q);
-        internalize_set(e, is_div ? quot : rem);        
+    void solver::internalize_udiv_i(app* e) {
+        expr* x, *y;
+        VERIFY(bv.is_bv_udivi(e, x, y) || bv.is_bv_udiv(e, x, y));
+        app_ref rm(bv.mk_bv_urem_i(x, y), m);
+        internalize(rm);
+    }
+
+    void solver::internalize_urem_i(app* e) {
+        expr* x, *y;
+        if (expr2enode(e))
+            return;
+        VERIFY(bv.is_bv_uremi(e, x, y) || bv.is_bv_urem(e, x, y));
+        auto [quot, rem] = quot_rem(x, y);
+        internalize_set(e, rem);
+        internalize_set(bv.mk_bv_udiv_i(x, y), quot);
+    }
+
+    std::pair<pdd, pdd> solver::quot_rem(expr* x, expr* y) {
+        pdd a = expr2pdd(x);
+        pdd b = expr2pdd(y);
+        auto& m = a.manager();
+        unsigned sz = m.power_of_2();
+        if (b.is_zero())
+            // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
+            return { m.mk_val(m.max_value()), a };
+
+        if (b.is_one())
+            return { a, m.zero() };
+
+        if (a.is_val() && b.is_val()) {
+            rational const av = a.val();
+            rational const bv = b.val();
+            SASSERT(!bv.is_zero());
+            rational rv;
+            rational qv = machine_div_rem(av, bv, rv);
+            pdd q = m.mk_val(qv);
+            pdd r = m.mk_val(rv);
+            SASSERT_EQ(a, b * q + r);
+            SASSERT(b.val() * q.val() + r.val() <= m.max_value());
+            SASSERT(r.val() <= (b * q + r).val());
+            SASSERT(r.val() < b.val());
+            return { std::move(q), std::move(r) };
+        }
+        
+        expr* quot = bv.mk_bv_udiv_i(x, y);
+        expr* rem = bv.mk_bv_urem_i(x, y);
+
+        ctx.internalize(quot);
+        ctx.internalize(rem);
+        auto quotv = expr2enode(quot)->get_th_var(get_id());
+        auto remv  = expr2enode(rem)->get_th_var(get_id());
+
+        pdd q = var2pdd(quotv);
+        pdd r = var2pdd(remv);
+
+        // Axioms for quotient/remainder
+        // 
+        //      a = b*q + r
+        //      multiplication does not overflow in b*q
+        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
+        //      b ≠ 0  ==>  r < b
+        //      b = 0  ==>  q = -1
+        // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
+        //       Maybe we need something like an op_constraint for better propagation.
+        add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false);
+        add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false);
+        // r <= b*q+r
+        //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
+        // b*q <= -r-1
+        add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false);
+
+        auto c_eq = m_core.eq(b);
+        if (!c_eq.is_always_true())
+            add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false);
+        if (!c_eq.is_always_false())
+            add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
+
+        return { std::move(q), std::move(r) };
     }
 
     void solver::internalize_div_rem(app* e, bool is_div) {
         bv_rewriter_params p(s().params());
         if (p.hi_div0()) {
-            internalize_div_rem_i(e, is_div);
+            if (bv.is_bv_udivi(e))
+                internalize_udiv_i(e);
+            else
+                internalize_urem_i(e);
             return;
         }
         expr* arg1 = e->get_arg(0);
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 8baf05de5..e4e022c6e 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -84,6 +84,8 @@ namespace polysat {
             }
         }
         }
+        UNREACHABLE();
+        return sat::check_result::CR_GIVEUP;
     }
 
     void solver::asserted(literal l) {
@@ -249,11 +251,11 @@ namespace polysat {
         return ctx.get_trail_stack();
     }
 
-    void solver::add_lemma(vector<signed_constraint> const& lemma) {
+    void solver::add_polysat_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant) {
         sat::literal_vector lits;
-        for (auto sc : lemma)
+        for (auto sc : cs)
             lits.push_back(ctx.mk_literal(constraint2expr(sc)));
-        s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
+        s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), nullptr));
     }
 
     void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
@@ -271,14 +273,14 @@ namespace polysat {
         case ckind_t::umul_ovfl_t: {
             auto l = pdd2expr(sc.to_umul_ovfl().p());
             auto r = pdd2expr(sc.to_umul_ovfl().q());
-            return expr_ref(bv.mk_bvumul_ovfl(l, r), m);
+            return expr_ref(m.mk_not(bv.mk_bvumul_no_ovfl(l, r)), m);
         }
         case ckind_t::smul_fl_t:
         case ckind_t::op_t:
             NOT_IMPLEMENTED_YET();
             break;
         }
-        throw default_exception("nyi"); 
+        throw default_exception("constraint2expr nyi"); 
     }
 
     expr_ref solver::pdd2expr(pdd const& p) {
@@ -346,7 +348,7 @@ namespace polysat {
                 continue;
             for (auto sib : euf::enode_class(p)) {
                 if (bv.is_extract(sib->get_expr(), lo, hi, e) && r == expr2enode(e)->get_root()) {
-                    throw default_exception("nyi");
+                    throw default_exception("get_fixed nyi");
                     // TODO                    
                     // dependency d = dependency(p->get_th_var(get_id()), n->get_th_var(get_id()), s().scope_lvl());
                     // fixed_bits.push_back({ hi, lo, rational::zero(), null_dependency()});
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index e1a9221e9..f2c80a6e6 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -113,10 +113,10 @@ namespace polysat {
         void internalize_extract(app* n);
         void internalize_repeat(app* n);
         void internalize_bit2bool(app* n);
-        void internalize_udiv_i(app* n);
         template<bool Signed, bool Reverse, bool Negated>
         void internalize_le(app* n);
-        void internalize_div_rem_i(app* e, bool is_div);
+        void internalize_udiv_i(app* e);
+        void internalize_urem_i(app* e);
         void internalize_div_rem(app* e, bool is_div);
         void internalize_polysat(app* a);
         void assert_bv2int_axiom(app * n);
@@ -126,6 +126,8 @@ namespace polysat {
         pdd var2pdd(euf::theory_var v);
         void internalize_set(expr* e, pdd const& p);
         void internalize_set(euf::theory_var v, pdd const& p);
+        std::pair<pdd, pdd> quot_rem(expr* x, expr* y);
+
 
         // callbacks from core
         void add_eq_literal(pvar v, rational const& val) override;
@@ -137,8 +139,7 @@ namespace polysat {
         bool inconsistent() const override;
         void get_bitvector_prefixes(pvar v, pvar_vector& out) override;
         void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) override;
-
-        void add_lemma(vector<signed_constraint> const& lemma);
+        void add_polysat_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
 
         std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);