diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 39c9879a6..0d83f155a 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -92,7 +92,7 @@ namespace euf {
             m_egraph.explain_eq<size_t>(m_explain, &m_explain_cc, a, b);
             m_egraph.end_explain();
             // Detect shortcut if equality is explained directly by a theory
-            if (m_explain.size() == 1 && !is_literal(m_explain[0])) {
+            if (m_explain.size() == 1 && is_justification(m_explain[0])) {
                 auto const& [x, y] = th_explain::from_index(get_justification(m_explain[0])).eq_consequent();
                 if (x == a && y == b)
                     continue;
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index b2be6439d..85d93bbdf 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -427,8 +427,8 @@ namespace polysat {
         unsigned sz = bv.get_bv_size(x);
         expr* u = bv.mk_bv_urem(x, y);
         rational N = rational::power_of_two(bv.get_bv_size(x));
-        expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
-        expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
+        expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x);
+        expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y);
         sat::literal lsignx = mk_literal(signx);
         sat::literal lsigny = mk_literal(signy);
         sat::literal u_eq0 = eq_internalize(u, bv.mk_zero(sz));
@@ -443,6 +443,22 @@ namespace polysat {
         add_axiom(name, { y_eq0, lsignx, lsigny, eq_internalize(e, u) });
     }
 
+    expr_ref solver::mk_ite(expr* c, expr* t, expr* e) {
+        expr_ref _c(c, m), _t(t, m), _e(e, m);
+        if (m.is_true(c))
+            return _t;
+        if (m.is_false(c))
+            return _e;
+        return expr_ref(m.mk_ite(c, t, e), m);
+    }
+
+    expr_ref solver::mk_ule(expr* l, expr* r) {
+        expr_ref res(bv.mk_ule(l, r), m);
+        ctx.get_rewriter()(res);
+        return res;
+    }
+
+
 
     // d = udiv(abs(x), abs(y))
     // y = 0, x > 0 -> 1
@@ -455,17 +471,19 @@ namespace polysat {
     void solver::axiomatize_sdiv(app* e, expr* x, expr* y) {
         unsigned sz = bv.get_bv_size(x);
         rational N = rational::power_of_two(bv.get_bv_size(x));
-        expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
-        expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
-        expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
-        expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
+        expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x);
+        expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y);
+        expr_ref absx = mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
+        expr_ref absy = mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
         expr* d = bv.mk_bv_udiv(absx, absy);
         sat::literal lsignx = mk_literal(signx);
         sat::literal lsigny = mk_literal(signy);
         sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
+        sat::literal x_eq0 = eq_internalize(x, bv.mk_zero(sz));
         auto name = "sdiv";
         add_axiom(name, { ~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz)) });
         add_axiom(name, { ~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N - 1, sz)) });
+        add_axiom(name, { y_eq0, ~x_eq0, eq_internalize(e, bv.mk_zero(sz)) });
         add_axiom(name, { y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d)) });
         add_axiom(name, { y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d)) });
         add_axiom(name, { y_eq0, lsignx, lsigny, eq_internalize(e, d) });
@@ -499,6 +517,7 @@ namespace polysat {
         euf::enode* rn = expr2enode(rem);
         auto& m = a.manager();
         unsigned sz = m.power_of_2();
+        verbose_stream() << "quot-rem " << a << " " << b << "\n";
         if (b.is_zero()) {
             // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
             internalize_set(quot, m.mk_val(m.max_value()));
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 17c57d263..1af7304e4 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -424,13 +424,22 @@ namespace polysat {
             if (q.is_zero() && p.has_unit(x)) {
                 auto l = pdd2expr(x);
                 auto r = pdd2expr(x - p);
-                result = m.mk_eq(l, r);
+                if (m.are_equal(l, r))
+                    result = m.mk_true();
+                else if (m.are_distinct(l, r))
+                    result = m.mk_false();
+                else 
+                    result = m.mk_eq(l, r);
             }
             else {
                 auto l = pdd2expr(p);
                 auto r = pdd2expr(q);
-                if (p == q)
+                if (m.are_equal(l, r))
                     result = m.mk_true();
+                else if (m.is_value(l) && m.is_value(r)) {
+                    result = bv.mk_ule(l, r);
+                    ctx.get_rewriter()(result);
+                }
                 else if (q.is_zero())
                     result = m.mk_eq(l, r);
                 else
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 837cea15a..5b45533cb 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -187,6 +187,8 @@ namespace polysat {
         void axiomatize_bv2int(app* e, expr* x);
         void axioms_for_extract(app* e);
         void axioms_for_concat(app* e);
+        expr_ref mk_ite(expr* c, expr* t, expr* e);
+        expr_ref mk_ule(expr* l, expr* r);
         expr* rotate_left(app* e, unsigned n, expr* x);
         unsigned m_delayed_axioms_qhead = 0;
         ptr_vector<app> m_delayed_axioms;