diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 1d784985c..8175a2dd8 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -165,6 +165,47 @@ namespace dd {
         return true;
     }
 
+    unsigned pdd_manager::min_parity(PDD p) {
+        if (m_semantics != mod2N_e)
+            return 0;
+
+        if (is_val(p)) {
+            rational v = val(p);
+            if (v.is_zero())
+                return m_power_of_2 + 1;
+            unsigned r = 0;
+            while (v.is_even() && v > 0)
+                r++, v /= 2;
+            return r;
+        }
+        PDD q = p;
+        while (!is_val(q))
+            q = lo(q);
+        unsigned p2 = val(q).trailing_zeros();
+        init_mark();
+        if (p2 == 0)
+            return 0;
+        init_mark();
+        m_todo.push_back(hi(p));
+        while (!m_todo.empty() && p2 != 0) {
+            PDD r = m_todo.back();
+            m_todo.pop_back();
+            if (is_marked(r)) 
+                continue;
+            set_mark(r);
+            if (!is_val(r)) {
+                m_todo.push_back(lo(r));
+                m_todo.push_back(hi(r));
+            }
+            else if (val(r).is_zero())
+                continue;
+            else if (val(r).trailing_zeros() < p2)
+                p2 = val(r).trailing_zeros();
+        }
+        m_todo.reset();
+        return p2;        
+    }
+
     pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
         return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
     }
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index e656cee35..4851626b2 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -255,6 +255,7 @@ namespace dd {
         inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); }
         inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); }
         bool is_never_zero(PDD p);
+        unsigned min_parity(PDD p);
         inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
         inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
         inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
@@ -432,6 +433,7 @@ namespace dd {
         void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
         vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
         bool is_never_zero() const { return m.is_never_zero(root); }
+        unsigned min_parity() const { return m.min_parity(root); }
         bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
         pdd operator-() const { return m.minus(*this); }
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index d7ba543eb..0884d9b9a 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -633,6 +633,7 @@ namespace polysat {
     bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) {
         set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))");
         auto& m = s.var2pdd(x);
+        unsigned N = m.power_of_2();
         pdd y = m.zero();
         pdd a = m.zero();
         pdd b = m.zero();
@@ -653,29 +654,78 @@ namespace polysat {
         LOG("a_is_odd: " << lit_pp(s, a_is_odd));
         LOG("x_is_odd: " << lit_pp(s, x_is_odd));
 #endif
-        if (!b_is_odd.is_currently_true(s)) {
-            if (!a_is_odd.is_currently_true(s))
-                return false;
-            if (!x_is_odd.is_currently_true(s))
-                return false;
+        if (a_is_odd.is_currently_true(s) &&
+            x_is_odd.is_currently_true(s)) {
             m_lemma.reset();
             m_lemma.insert_eval(~s.eq(y));
             m_lemma.insert_eval(~a_is_odd);
             m_lemma.insert_eval(~x_is_odd);
             if (propagate(core, axb_l_y, b_is_odd))
                 return true;
-            return false;
         }
-        m_lemma.reset();
-        m_lemma.insert_eval(~s.eq(y));
-        m_lemma.insert_eval(~b_is_odd);
-        if (propagate(core, axb_l_y, a_is_odd))
-            return true;
-        m_lemma.reset();
-        m_lemma.insert_eval(~s.eq(y));
-        m_lemma.insert_eval(~b_is_odd);
-        if (propagate(core, axb_l_y, x_is_odd))
-            return true;
+
+#if 0
+        // TODO - enable this code and test
+        // a is divisibly by 4,
+        // max divisor of x is k
+        // -> b has parity k + 4
+        if ((~a_is_odd).is_currently_true(s) || 
+            (~x_is_odd).is_currently_true(s)) {
+            unsigned a_parity = 0;
+            unsigned x_parity = 0;
+            while (a_parity <= N && s.parity(a, a_parity+1).is_currently_true(s))
+                ++a_parity;
+            while (x_parity <= N && s.parity(X, x_parity+1).is_currently_true(s))
+                ++x_parity;
+            SASSERT(a_parity > 0 || x_parity > 0);
+            unsigned b_parity = std::min(N + 1, a_parity + x_parity);
+            if (a_parity > 0)
+                m_lemma.insert_eval(~s.parity(a, a_parity));
+            if (x_parity > 0)
+                m_lemma.insert_eval(~s.parity(X, x_parity));
+            if (propagate(core, axb_l_y, s.parity(b, b_parity)))
+                return true;
+        }
+#endif
+
+        if (b_is_odd.is_currently_true(s)) {
+            m_lemma.reset();
+            m_lemma.insert_eval(~s.eq(y));
+            m_lemma.insert_eval(~b_is_odd);
+            if (propagate(core, axb_l_y, a_is_odd))
+                return true;
+            m_lemma.reset();
+            m_lemma.insert_eval(~s.eq(y));
+            m_lemma.insert_eval(~b_is_odd);
+            if (propagate(core, axb_l_y, x_is_odd))
+                return true;
+        }
+
+#if 0
+
+        // 
+        // if b has at least b_parity, then a*x has at least b_parity
+        // establish lower bound on parity of b
+        // 
+        if ((~b_is_odd).is_currently_true(s) && !is_forced_eq(b, 0)) {
+            unsigned b_parity = 1;
+            while (b_parity <= N && s.parity(b, b_parity+1).is_currently_true(s))
+                ++b_parity;
+            SASSERT(b_parity <= N);
+            // TODO:
+            // something like this (but fixed)
+            for (unsigned i = 0; i <= b_parity; ++i) {
+                if (s.parity(a, b_parity - i).is_currently_false(s)) {
+                    m_lemma.reset();
+                    m_lemma.insert_eval(~s.eq(y));
+                    m_lemma.insert_eval(~s.parity(b, b_parity));
+                    m_lemma.insert_eval(s.parity(a, b_parity - i));
+                    if (propagate(core, axb_l_y, s.parity(x, i)))
+                        return true;
+                }
+            }
+        }
+#endif
         return false;        
     }
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 1af414a14..aeeafba0e 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -413,7 +413,15 @@ namespace polysat {
         signed_constraint odd(pdd const& p) { return ~even(p); }
         signed_constraint even(pdd const& p) { return parity(p, 1); }
         /** parity(p) >= k   (<=> p * 2^(K-k) == 0) */
-        signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); }
+        signed_constraint parity(pdd const& p, unsigned k) {            
+            unsigned N = p.manager().power_of_2();
+            if (k > N)
+                return eq(p);
+            else if (k == 0)
+                return odd(p);
+            else 
+                return eq(p*rational::power_of_two(N - k));
+        }
         signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
         signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); }
         signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }