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/viable.cpp b/src/math/polysat/viable.cpp
index 362054e59..c09330009 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -190,7 +190,7 @@ namespace polysat {
                     lo = val;
                 }
                 SASSERT(hi <= s.var2pdd(v).max_value());
-                LOG("forbidden interval [" << lo << ", " << hi << "[\n");
+                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);