diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 23b4c1f8e..436eb7130 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -33,7 +33,7 @@ namespace polysat {
         for (auto c1 : core) {
             if (!c1->is_ule())
                 continue;
-            if (!c1.is_currently_false(s))
+            if (c1.is_currently_true(s))
                 continue;
             auto c = c1.as_inequality();
             if (try_ugt_x(v, core, c))
@@ -70,7 +70,7 @@ namespace polysat {
         SASSERT(!crit1.is_currently_true(s));
 
         LOG("critical " << m_rule << " " << crit1);
-        LOG("consequent " << c << " value: " << c.bvalue(s) << " " << c.is_currently_false(s) << " " << core.contains(~c));
+        LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c));
 
 
         // ensure new core is a conflict
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 356506be0..dd9b526b8 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -61,7 +61,7 @@ namespace polysat {
 
     void search_state::pop() {
         auto const& item = m_items.back();
-        if (item.is_assignment() && item.var() == m_assignment.back().first) 
+        if (item.is_assignment() && !m_assignment.empty() && item.var() == m_assignment.back().first) 
             m_assignment.pop_back();        
         m_items.pop_back();
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index bd6ca895b..b773eac64 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -456,10 +456,16 @@ namespace polysat {
         ++m_stats.m_num_conflicts;
 
         SASSERT(is_conflict());
-
+        
         if (m_conflict.conflict_var() != null_var) {
+            pvar v = m_conflict.conflict_var();
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
-            VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));           
+            VERIFY(m_viable.resolve(v, m_conflict));
+            // TBD: saturate resulting conflict to get better lemmas.
+            LOG("try-saturate");
+            m_conflict.try_saturate(v);
+            LOG("end-try-saturate");
+>>>>>>> ed9c0b84f668548ee1c11f14185b08333baa6f72
         }
 
         search_iterator search_it(m_search);
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 3beb72e87..7a71a2d48 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -198,7 +198,7 @@ namespace polysat {
                     lo = val - lambda_l;                   
                 }
                 SASSERT(hi <= s.var2pdd(v).max_value());
-                LOG("forbidden interval " << e->interval << " [" << lo << ", " << hi << "[");
+                LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "[");
                 entry* ne = alloc_entry();
                 ne->src = e->src;
                 ne->side_cond = e->side_cond;
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 51e2567d3..65cac43f4 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1065,10 +1065,17 @@ namespace polysat {
 
 void tst_polysat() {
 
-
-    polysat::test_l5();
+    polysat::test_ineq_axiom1();
+    polysat::test_ineq_axiom2();
+    polysat::test_ineq_axiom3();
+    polysat::test_ineq_axiom4();
+    polysat::test_ineq_axiom5();
+    polysat::test_ineq_axiom6();
     return;
 
+    polysat::test_ineq_basic4();
+    //return;
+
     polysat::test_ineq_basic6();
             
     // polysat::test_monot_bounds(8);