diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp
index 8c1e3f703..8217f68a7 100644
--- a/src/sat/smt/polysat/constraints.cpp
+++ b/src/sat/smt/polysat/constraints.cpp
@@ -88,6 +88,10 @@ namespace polysat {
             return eq(p * rational::power_of_two(N - k));
     }
 
+    signed_constraint constraints::parity_at_most(pdd const& p, unsigned k) {
+        return ~parity_at_least(p, k + 1);
+    }
+
     // 2^{N-i-1}* p >= 2^{N-1}
     signed_constraint constraints::bit(pdd const& p, unsigned i) {
         unsigned N = p.manager().power_of_2();
diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h
index 8dbf150a5..7e54126eb 100644
--- a/src/sat/smt/polysat/constraints.h
+++ b/src/sat/smt/polysat/constraints.h
@@ -169,6 +169,7 @@ namespace polysat {
         signed_constraint umul_ovfl(unsigned        p, pdd const& q) { return umul_ovfl(rational(p), q); }
 
         signed_constraint parity_at_least(pdd const& p, unsigned k);
+        signed_constraint parity_at_most(pdd const& p, unsigned k);
 
         signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r);
         signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r);
diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp
index 52ab0c4bf..9b78e6a94 100644
--- a/src/sat/smt/polysat/monomials.cpp
+++ b/src/sat/smt/polysat/monomials.cpp
@@ -66,12 +66,12 @@ namespace polysat {
             return l_false;
         if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
             return l_false;
-        if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
+        if (any_of(m_to_refine, [&](auto i) { return mul_parametric_inverse(m_monomials[i]); }))
             return l_false;
 
-        if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); }))
+        if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
             return l_false;
-        if (any_of(m_to_refine, [&](auto i) { return non_overflow_zero(m_monomials[i]); }))
+        if (any_of(m_to_refine, [&](auto i) { return mul0_inverse(m_monomials[i]); }))
             return l_false;
         if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
             return l_false;
@@ -171,19 +171,32 @@ namespace polysat {
         return c.add_axiom("p = k => p * q = k * q", cs, true);
     }
 
-    // p * q = p => q = 1 or p = 0
-    //
-    // In general not true, because there exist a, b >= 2 with a * b = 0; then (a+1) * b = b.
-    // For now, add no-overflow condition on p*q.
-    bool monomials::mul1_inverse(monomial const& mon) {
+    // p * q = p => parity(q - 1) + parity(p) >= N
+    // p * q = p & ~Ovfl(p,q) => q = 1 or p = 0
+    bool monomials::mul_parametric_inverse(monomial const& mon) {
         for (unsigned j = mon.size(); j-- > 0; ) {
             auto const& arg_val = mon.arg_vals[j];
             if (arg_val == mon.val) {
                 auto const& p = mon.args[j];
                 pdd qs = c.value(rational(1), mon.num_bits());
+                rational qv(1);
                 for (unsigned k = mon.size(); k-- > 0; ) 
-                    if (k != j)
-                        qs *= mon.args[k];
+                    if (k != j) 
+                        qs *= mon.args[k], qv *= mon.arg_vals[k];
+
+                if (qv == 0) {
+                    if (c.add_axiom("q = 0 & p * q = p => p = 0", { ~C.eq(qs), ~C.eq(mon.var, p), C.eq(p)}, true))
+                        return true;
+                    continue;
+                }
+                qv = qv - 1;
+                unsigned qb = qv.get_num_bits();
+                unsigned pb = arg_val.get_num_bits();
+                unsigned N = p.manager().power_of_2();
+                if (qb + pb < N) {
+                    if (c.add_axiom("p * q = p => parity(q - 1) + parity(p) >= N", { ~C.eq(mon.var, p), ~C.parity_at_most(p, pb), C.parity_at_least(qs - 1, N - pb) }, true))
+                        return true;
+                }
                 if (c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true))
                     return true;
             }
@@ -234,8 +247,21 @@ namespace polysat {
         return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
     }
 
+    // p * q = 1 => parity(p) = 0 (instance of parity(p*q) >= min(N, parity(p) + parity(q))
     // ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1
-    bool monomials::non_overflow_unit(monomial const& mon) {
+    bool monomials::mul1_inverse(monomial const& mon) {
+        if (!mon.val.is_odd())
+            return false;
+
+        unsigned j = 0;
+        for (auto const& val : mon.arg_vals) {
+            if (val.is_even()) {
+                if (c.add_axiom("odd(p*q) => odd(p)",
+                    {~C.parity_at_most(mon.var, 0), C.parity_at_most(mon.args[j], 0) }, true))
+                    return true;
+            }
+            ++j;
+        }
         if (mon.val != 1)
             return false;
         rational product(1);
@@ -260,8 +286,11 @@ namespace polysat {
         return new_axiom;
     }
 
+
+    // p*q = 0 => parity(p) + parity(q) >= N
+    // TODO: update to use parity instead of overflow
     // ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0
-    bool monomials::non_overflow_zero(monomial const& mon) {
+    bool monomials::mul0_inverse(monomial const& mon) {
         if (mon.val != 0)
             return false;
         for (auto const& val : mon.arg_vals)
diff --git a/src/sat/smt/polysat/monomials.h b/src/sat/smt/polysat/monomials.h
index 779def053..d88b80543 100644
--- a/src/sat/smt/polysat/monomials.h
+++ b/src/sat/smt/polysat/monomials.h
@@ -49,12 +49,12 @@ namespace polysat {
         bool mul0(monomial const& mon);
         bool mul1(monomial const& mon);
         bool mulp2(monomial const& mon);
-        bool mul1_inverse(monomial const& mon);
+        bool mul_parametric_inverse(monomial const& mon);
         bool mul(monomial const& mon, std::function<bool(rational const&)> const& p);
         bool parity(monomial const& mon);
         bool non_overflow_monotone(monomial const& mon);
-        bool non_overflow_unit(monomial const& mon);
-        bool non_overflow_zero(monomial const& mon);
+        bool mul1_inverse(monomial const& mon);
+        bool mul0_inverse(monomial const& mon);
         bool parity0(monomial const& mon);
         bool prefix_overflow(monomial const& mon);
 
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 583fa30b3..8f1c6f0c5 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -268,7 +268,7 @@ namespace polysat {
                 add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}", 
                     { d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) },
                     true);
-            }
+            }            
             else if (bx + by > N + 1) 
                 add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k - 1", 
                     {d, ~msb_ge(x, k), msb_le(y, N - k - 1)},
@@ -276,11 +276,9 @@ namespace polysat {
             else {
                 auto x1 = c.mk_zero_extend(1, x);
                 auto y1 = c.mk_zero_extend(1, y);                
-                add_clause("~Ovfl(x, y) & msb(x) >= k & msb(y) >= N - k - 1 => 0x * 0y < 2^{N-1}",
-                    { d, ~msb_ge(x, k),
-                         ~msb_ge(y, N - k - 1),
-                         C.ult(x1 * y1, rational::power_of_two(N - 1))
-                    }, true);
+                add_clause("~Ovfl(x, y) => 0x * 0y < 2^{N}",
+                    { d, C.ult(x1 * y1, rational::power_of_two(N)) }, 
+                    true);
             }
         }
         else {
@@ -303,7 +301,7 @@ namespace polysat {
                 auto k = bx - 1;
                 auto x1 = c.mk_zero_extend(1, x);
                 auto y1 = c.mk_zero_extend(1, y);
-                add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 = > 0x * 0y >= 2 ^ {N - 1}",
+                add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 => 0x * 0y >= 2 ^ {N - 1}",
                     { d, ~msb_le(x, k), ~msb_le(y, N - k - 1), C.uge(x1 * y1, rational::power_of_two(N - 1)) },
                     true);
             }