diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index 8c585256e..cc8770f05 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -61,6 +61,7 @@ namespace polysat {
     void clause_builder::push(signed_constraint c) {
         SASSERT(c);
         SASSERT(c->has_bvar());
+        SASSERT(!c.is_always_false());   // if this case occurs legitimately, we should skip the constraint.
         if (c.is_always_true()) {
             m_is_tautology = true;
             return;
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 2a04d8386..389a091a1 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -240,6 +240,7 @@ namespace polysat {
     *   and division with coeff are valid. Is there a more relaxed scheme?
     */
     bool viable::refine_equal_lin(pvar v, rational const& val) {
+        // LOG_H2("refine-equal-lin with v" << v << ", val = " << val);
         auto* e = m_equal_lin[v];
         if (!e)
             return true;
@@ -283,8 +284,25 @@ namespace polysat {
             }
         };
         do {
+            LOG("refine-equal-lin for src: " << e->src);
             rational coeff_val = mod(e->coeff * val, mod_value);
             if (e->interval.currently_contains(coeff_val)) {
+
+                if (e->interval.lo_val().is_one() && e->interval.hi_val().is_zero() && e->coeff.is_odd()) {
+                    rational lo(1);
+                    rational hi(0);
+                    LOG("refine-equal-lin: " << " [" << lo << ", " << hi << "[");
+                    pdd lop = s.var2pdd(v).mk_val(lo);
+                    pdd hip = s.var2pdd(v).mk_val(hi);
+                    entry* ne = alloc_entry();
+                    ne->src = e->src;
+                    ne->side_cond = e->side_cond;
+                    ne->coeff = 1;
+                    ne->interval = eval_interval::proper(lop, lo, hip, hi);
+                    intersect(v, ne);
+                    return false;
+                }
+
                 rational lo = val - delta_l(coeff_val);
                 rational hi = val + delta_u(coeff_val) + 1;