diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index cbc7d4040..961ee6839 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -165,10 +165,9 @@ namespace polysat {
             auto c2 = s.ule(a, b);
             if (!c.is_positive())
                 c2 = ~c2;
-            LOG("try-reduce is false " << c2.is_currently_false(s));
             if (!c2.is_currently_false(s))
                 continue;
-            if (c2.bvalue(s) == l_false)
+            if (c2.is_always_false() || c2.bvalue(s) == l_false)
                 return false;
             if (!c2->has_bvar() || l_undef == c2.bvalue(s)) {
                 vector<signed_constraint> premises;
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index 63b97ed5b..0007abf08 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -73,11 +73,9 @@ namespace polysat {
         // a*v <= 0, a odd
         if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
-
         // a*v + b > 0, a odd
         if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
-
         if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
         if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@@ -349,7 +347,7 @@ namespace polysat {
         signed_constraint const& c,
         rational const & a1, pdd const& b1, pdd const& e1,
         fi_record& fi) {
-        if (a1.is_odd() && b1.is_zero() && !c.is_positive()) {
+        if (a1.is_odd() && b1.is_zero() && c.is_negative()) {
             auto& m = e1.manager();
             rational lo_val(0);
             auto lo = m.zero();
@@ -361,7 +359,7 @@ namespace polysat {
                 fi.side_cond.push_back(s.eq(b1, e1));
             return true;
         }
-        if (a1.is_odd() && b1.is_val() && !c.is_positive()) {
+        if (a1.is_odd() && b1.is_val() && c.is_negative()) {
             auto& m = e1.manager();
             rational const& mod_value = m.two_to_N();
             rational a1_inv;
@@ -389,7 +387,7 @@ namespace polysat {
         signed_constraint const& c,
         rational const & a2, pdd const& b2, pdd const& e2,
         fi_record& fi) {
-        if (a2.is_one() && b2.is_val() && !c.is_positive()) {
+        if (a2.is_one() && b2.is_val() && c.is_negative()) {
             auto& m = e2.manager();
             rational const& mod_value = m.two_to_N();
             rational lo_val(mod(-b2.val() - 1, mod_value));
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 7c24241ef..2a24f7551 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -46,9 +46,11 @@ namespace polysat {
 
     void viable::pop_viable() {
         auto& [v, k, e] = m_trail.back();
+        SASSERT(well_formed(m_units[v]));
         switch (k) {
         case entry_kind::unit_e: 
             e->remove_from(m_units[v], e); 
+            SASSERT(well_formed(m_units[v]));
             break;
         case entry_kind::equal_e: 
             e->remove_from(m_equal_lin[v], e); 
@@ -67,13 +69,15 @@ namespace polysat {
         SASSERT(e->prev() != e || e->next() == e);
         SASSERT(k == entry_kind::unit_e);
         (void)k;
+        SASSERT(well_formed(m_units[v]));
         if (e->prev() != e) {
             e->prev()->insert_after(e);
-            if (e->interval.lo_val() < e->next()->interval.lo_val())
+            if (e->interval.lo_val() < m_units[v]->interval.lo_val())
                 m_units[v] = e;
         }
         else 
-            m_units[v] = e;        
+            m_units[v] = e;  
+        SASSERT(well_formed(m_units[v]));
         m_trail.pop_back();
     }
 
@@ -102,6 +106,7 @@ namespace polysat {
     }
 
     void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
+        SASSERT(well_formed(m_units[v]));
         m_trail.push_back({ v, k, e });
         s.m_trail.push_back(trail_instr_t::viable_add_i);
         e->init(e);
@@ -109,6 +114,7 @@ namespace polysat {
             entries[v] = e;
         else
             e->insert_after(entries[v]);
+        SASSERT(well_formed(m_units[v]));
     }
 
     bool viable::intersect(pvar v, entry* ne) {
@@ -441,6 +447,7 @@ namespace polysat {
         return refine_viable(v, val);
     }
 
+
     rational viable::min_viable(pvar v) { 
         refined:
         rational lo(0);
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 8ce90bf7f..068269269 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1375,10 +1375,6 @@ namespace polysat {
 void tst_polysat() {
     using namespace polysat;
 
-    test_polysat::test_ineq1();
-    test_polysat::test_ineq2();
-    test_polysat::test_monot();
-    return;
 
     test_polysat::test_fi_zero();
     test_polysat::test_fi_nonzero();