diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 40b7e6d1a..12b80088c 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -287,7 +287,7 @@ namespace polysat {
         if (c.is_always_true())
             return;
         LOG("Inserting " << lit_pp(s, c));
-        SASSERT(c.bvalue(s) == l_true);
+        SASSERT_EQ(c.bvalue(s), l_true);
         SASSERT(!c.is_always_false());  // if we added c, the core would be a tautology
         SASSERT(!c->vars().empty());
         m_literals.insert(c.blit().index());
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index efa1317b9..a7b1d4a0a 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -102,7 +102,7 @@ namespace polysat {
             core.insert_eval(d);
         if (c.bvalue(s) != l_false)  // conflict is due to the evaluation of c, so it depends on the variable values
             core.insert_vars(c);
-        core.insert(~c);
+        core.insert_eval(~c);
         core.set_backjump();
         core.logger().log(inf_name);
         LOG("Core " << core);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 58f55df22..ac581f385 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -246,6 +246,7 @@ namespace polysat {
     */
     void solver::propagate(sat::literal lit) {
         LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
+        LOG("Literal " << lit_pp(*this, lit));
         signed_constraint c = lit2cnstr(lit);
         SASSERT(c);
         // TODO: review active and activate_constraint
@@ -471,6 +472,7 @@ namespace polysat {
             case trail_instr_t::pwatch_i: {
                 constraint* c = m_pwatch_trail.back();
                 erase_pwatch(c);
+                c->set_active(false);   // TODO: review meaning of "active"
                 m_pwatch_trail.pop_back();
                 break;
             }
@@ -789,7 +791,7 @@ namespace polysat {
      */
     void solver::revert_decision(pvar v) {
         rational val = m_value[v];
-        LOG_H3("Reverting decision: pvar " << v << " := " << val);
+        LOG_H2("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
 
         clause_ref lemma = m_conflict.build_lemma();
@@ -1015,6 +1017,10 @@ namespace polysat {
         }
         if (c->is_pwatched())
             out << " pwatched";
+        if (c->is_active())
+            out << " active";
+        if (c->is_external())
+            out << " ext";
         out << " ]";
         return out;
     }
@@ -1087,8 +1093,8 @@ namespace polysat {
             }
             unsigned expected_watches = std::min(2u, c->vars().size());
             if (num_watches != expected_watches)
-                LOG("wrong number of watches: " << sc.blit() << ": " << sc << " (vars: " << sc->vars() << ")");
-            SASSERT_EQ(num_watches, expected_watches);
+                LOG("Wrong number of watches: " << sc.blit() << ": " << sc << " (vars: " << sc->vars() << ")");
+            VERIFY_EQ(num_watches, expected_watches);
         }
         return true;
     }
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 5f5ff4d77..17e6e7b13 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -232,6 +232,14 @@ namespace polysat {
             s.expect_sat({{a, 4}, {b, 4}});
         }
 
+        static void test_l6() {
+            scoped_solver s(__func__);
+            auto x = s.var(s.add_var(6));
+            s.add_ule(29*x + 3, 29*x + 1);
+            s.check();
+            s.expect_sat();
+        }
+
         /**
          * This one is unsat because a*a*(a*a - 1)
          * is 0 for all values of a.
@@ -1404,7 +1412,7 @@ void tst_polysat() {
     // test_polysat::test_add_conflicts();  // ok
     // test_polysat::test_wlist();  // ok
     // test_polysat::test_cjust();  // uses viable_fallback; weak lemmas
-    // test_polysat::test_subst();  // TODO: assert + resource limit
+    // test_polysat::test_subst();  // TODO: resource limit; needs polynomial superposition
     // test_polysat::test_pop_conflict();  // ok now (had bad conflict/pop interaction)
 
     // test_polysat::test_l1();   // ok
@@ -1413,13 +1421,14 @@ void tst_polysat() {
     // test_polysat::test_l4();   // ok now (had assertion failure in conflict::insert)
     // test_polysat::test_l4b();  // ok
     // test_polysat::test_l5();   // inefficient conflicts (needs equality reasoning)
+    // test_polysat::test_l6();   // ok (refine-equal-lin)
 
     // test_polysat::test_p1();    // ok (conflict @0 by viable_fallback)
     // test_polysat::test_p2();    // ok (viable_fallback finds the correct value)
     // test_polysat::test_p3();    // TODO: resource limit
 
     // test_polysat::test_ineq_basic1();  // ok
-    // test_polysat::test_ineq_basic2();  // TODO: assert / boolean conflict
+    // test_polysat::test_ineq_basic2();  // ok
     // test_polysat::test_ineq_basic3();  // ok
     // test_polysat::test_ineq_basic4();  // TODO: resource limit
     // test_polysat::test_ineq_basic5();  // works, but only because variable order changes after the conflict
@@ -1436,7 +1445,7 @@ void tst_polysat() {
     // test_polysat::test_monot_bounds(2);  // weak conflicts
     // test_polysat::test_monot_bounds(8);
     // test_polysat::test_monot_bounds();  // TODO: resource limit
-    // test_polysat::test_monot_bounds_full();  // TODO: triggers assertion in watchlist invariant
+    // test_polysat::test_monot_bounds_full();  // TODO: triggers assertion in watchlist invariant -- it's a problem with push/pop and that the "active" flag isn't maintained properly
     // test_polysat::test_monot_bounds_simple(8);  // undef
     // test_polysat::test_fixed_point_arith_div_mul_inverse();   // undef