diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 96869bbe9..5f5cb8caa 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -183,7 +183,7 @@ namespace polysat {
     }
 
     void inf_saturate::push_omega(pdd const& x, pdd const& y) {     
-        m_new_constraints.insert(~s.mul_ovfl(x, y));
+        m_new_constraints.insert(~s.umul_ovfl(x, y));
         /*
         // determine worst case upper bounds for x, y
         // then extract premises for a non-worst-case bound.
diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp
index 6dc04e2ad..8a4474189 100644
--- a/src/math/polysat/smul_fl_constraint.cpp
+++ b/src/math/polysat/smul_fl_constraint.cpp
@@ -80,13 +80,13 @@ namespace polysat {
                 s.add_clause(~sc, s.ule(2, q()), false);
                 s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(q(), 0), false);
                 s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p(), 0), false);
-                s.add_clause(~sc, ~s.sgt(p(), 0), s.slt(p()*q(), 0), s.mul_ovfl(p(), q()), false);
-                s.add_clause(~sc, s.sgt(p(), 0),  s.slt(p()*q(), 0), s.mul_ovfl(-p(), -q()), false);
+                s.add_clause(~sc, ~s.sgt(p(), 0), s.slt(p()*q(), 0), s.umul_ovfl(p(), q()), false);
+                s.add_clause(~sc, s.sgt(p(), 0),  s.slt(p()*q(), 0), s.umul_ovfl(-p(), -q()), false);
             }
             else {
-                s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.mul_ovfl(p(), q()), false);
+                s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.umul_ovfl(p(), q()), false);
                 s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.slt(p()*q(), 0), false);
-                s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.mul_ovfl(-p(), -q()), false);
+                s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.umul_ovfl(-p(), -q()), false);
                 s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.slt((-p())*(-q()), 0), false);
             }
         }
@@ -96,13 +96,13 @@ namespace polysat {
                 s.add_clause(~sc, s.ule(2, q()), false);
                 s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), false);
                 s.add_clause(~sc, s.sgt(q(), 0), s.sgt(p(), 0), false);
-                s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(p(), -q()), false);
-                s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(-p(), q()), false);
+                s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(p()*q(), 0), s.umul_ovfl(p(), -q()), false);
+                s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p()*q(), 0), s.umul_ovfl(-p(), q()), false);
             }
             else {
-                s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.mul_ovfl(p(), -q()), false);
+                s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.umul_ovfl(p(), -q()), false);
                 s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false);
-                s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.mul_ovfl(-p(), q()), false);
+                s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.umul_ovfl(-p(), q()), false);
                 s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);                
             }                
         }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index adceb7619..52f2655ff 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -150,7 +150,7 @@ namespace polysat {
         //      b ≠ 0  ==>  r < b
         //      b = 0  ==>  q = -1
         add_eq(a, b * q + r);
-        add_noovfl(b, q);
+        add_umul_noovfl(b, q);
         add_ule(r, b*q+r);
 
         auto c_eq = eq(b);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 22e4ad5f2..ee6d2ff89 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -263,7 +263,19 @@ namespace polysat {
          * retrieve unsat core dependencies
          */
         void unsat_core(dependency_vector& deps);
-        
+
+        /**
+         * Return value / level of v in the current model (only meaningful if check_sat() returned l_true).
+         */
+        rational get_value(pvar v) const { SASSERT(is_assigned(v)); return m_value[v]; }
+
+        unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
+
+        /**
+         * Evaluate term under the current assignment.
+         */
+        bool try_eval(pdd const& p, rational& out_value) const;
+
         /**
          * Add variable with bit-size. 
          */
@@ -301,25 +313,11 @@ namespace polysat {
          */
         pdd value(rational const& v, unsigned sz);
 
-        /**
-         * Return value / level of v in the current model (only meaningful if check_sat() returned l_true).
-         */
-        rational get_value(pvar v) const { SASSERT(is_assigned(v)); return m_value[v]; }
-
-        unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
-
-
-        /**
-         * Evaluate term under the current assignment.
-         */
-        bool try_eval(pdd const& p, rational& out_value) const;
-
         /**
          * Apply current substitution to p.
          */
         pdd subst(pdd const& p) const; 
 
-
         /** Create constraints */
         signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
         signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); }
@@ -346,8 +344,8 @@ namespace polysat {
         signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); }
         signed_constraint sgt(pdd const& p, int n) { return slt(n, p); }
         signed_constraint sgt(int n, pdd const& p) { return slt(p, n); }
-        signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); }
-        signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_ovfl(q.manager().mk_val(p), q); }
+        signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); }
+        signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); }
         signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); }
         signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
         signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
@@ -365,8 +363,8 @@ namespace polysat {
         void add_ult(pdd const& p, pdd const& q, dependency dep = null_dependency)          { assign_eh(ult(p, q), dep); }
         void add_sle(pdd const& p, pdd const& q, dependency dep = null_dependency)          { assign_eh(sle(p, q), dep); }
         void add_slt(pdd const& p, pdd const& q, dependency dep = null_dependency)          { assign_eh(slt(p, q), dep); }
-        void add_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency)       { assign_eh(~mul_ovfl(p, q), dep); }
-        void add_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency)         { assign_eh(mul_ovfl(p, q), dep); }
+        void add_umul_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency)  { assign_eh(~umul_ovfl(p, q), dep); }
+        void add_umul_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency)    { assign_eh(umul_ovfl(p, q), dep); }
 
         void add_ule(pdd const& p, rational const& q, dependency dep = null_dependency)     { add_ule(p, p.manager().mk_val(q), dep); }
         void add_ule(rational const& p, pdd const& q, dependency dep = null_dependency)     { add_ule(q.manager().mk_val(p), q, dep); }
@@ -376,10 +374,10 @@ namespace polysat {
         void add_ult(rational const& p, pdd const& q, dependency dep = null_dependency)     { add_ult(q.manager().mk_val(p), q, dep); }
         void add_ult(pdd const& p, unsigned q, dependency dep = null_dependency)            { add_ult(p, rational(q), dep); }
         void add_ult(unsigned p, pdd const& q, dependency dep = null_dependency)            { add_ult(rational(p), q, dep); }
-        void add_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency)  { add_noovfl(p, p.manager().mk_val(q), dep); }
-        void add_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency)  { add_noovfl(q, p, dep); }
-        void add_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency)         { add_noovfl(p, rational(q), dep); }
-        void add_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency)         { add_noovfl(q, p, dep); }
+        void add_umul_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency)  { add_umul_noovfl(p, p.manager().mk_val(q), dep); }
+        void add_umul_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency)  { add_umul_noovfl(q, p, dep); }
+        void add_umul_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency)         { add_umul_noovfl(p, rational(q), dep); }
+        void add_umul_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency)         { add_umul_noovfl(q, p, dep); }
 
         /**
          * Activate the constraint corresponding to the given boolean variable.
diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index 7d05d97ab..0ba67825b 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -58,7 +58,7 @@ namespace bv {
         case OP_UGT:              polysat_le<false, false, true>(a); break;
         case OP_SGT:              polysat_le<true,  false, true>(a); break;
 
-        case OP_BUMUL_NO_OVFL:    mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.mul_ovfl(p, q); }); break;            
+        case OP_BUMUL_NO_OVFL:    mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.umul_ovfl(p, q); }); break;            
         case OP_BSMUL_NO_OVFL:    mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break;
         case OP_BSMUL_NO_UDFL:    mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break;