diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index 809793d94..9715de223 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -135,18 +135,22 @@ namespace polysat {
     }
 
     /**
-     * A literal may be watched if there is no unwatched literal that has been assigned later,
-     * where true and unassigned literals are considered at infinite level.
-     * We prefer true literals to unassigned literals.
+     * Priority for watching literals:
+     * 1. true literal, prefer lower search index to keep clause inactive for as long as possible.
+     * 2. unassigned literal
+     * 3. false literal, prefer higher search index (otherwise we might miss boolean propagations)
      */
     uint64_t bool_var_manager::get_watch_level(sat::literal lit) const {
         switch (value(lit)) {
-            case l_false:
-                return s.m_search.get_bool_index(lit);
-            case l_true:
-                return std::numeric_limits<uint64_t>::max();
-            case l_undef:
-                return std::numeric_limits<uint64_t>::max() - 1;
+        case l_true:
+            // 0xFFFF'FFFF'****'****
+            return 0xFFFF'FFFF'FFFF'FFFFull - s.m_search.get_bool_index(lit);
+        case l_undef:
+            // 0x0FFF'FFFF'FFFF'FFFF
+            return 0x0FFF'FFFF'FFFF'FFFFull;
+        case l_false:
+            // 0x0000'0000'****'****
+            return s.m_search.get_bool_index(lit);
         }
         UNREACHABLE();
         return 0;
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 707f585a9..26f309a77 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -276,9 +276,10 @@ namespace polysat {
         SASSERT(!s.is_assigned(v));
         m_level = s.m_level;
         logger().begin_conflict(header_with_var("viable_interval v", v));
-        VERIFY(s.m_viable.resolve_interval(v, *this));
+        if (s.m_viable.resolve_interval(v, *this)) {
+            revert_pvar(v);  // at this point, v is not assigned
+        }
         SASSERT(!empty());
-        revert_pvar(v);  // at this point, v is not assigned
     }
 
     void conflict::init_by_viable_fallback(pvar v, univariate_solver& us) {
@@ -319,6 +320,7 @@ namespace polysat {
     }
 
     bool conflict::insert_or_replace(signed_constraint c) {
+        // TODO: what if we have already passed c in the trail in resolve_conflict? should check that. (probably restart the resolve_conflict loop with the new conflict?)
         switch (c.bvalue(s)) {
         case l_true:
             // regular case
diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 46cf0738f..caca1e831 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -397,12 +397,12 @@ namespace polysat {
         //      b = 0  ==>  q = -1
         // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
         //       Maybe we need something like an op_constraint for better propagation.
-        s.add_clause(eq(b * q + r - a), false);
-        s.add_clause(~umul_ovfl(b, q), false);
+        s.add_clause("[axiom] quot_rem 1", { eq(b * q + r - a) }, false);
+        s.add_clause("[axiom] quot_rem 2", { ~umul_ovfl(b, q)  }, false);
         // r <= b*q+r
         //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
         // b*q <= -r-1
-        s.add_clause(ule(b*q, -r-1), false);
+        s.add_clause("[axiom] quot_rem 3", { ule(b*q, -r-1)    }, false);
 #if 0
         // b*q <= b*q+r
         //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
@@ -411,8 +411,8 @@ namespace polysat {
 #endif
 
         auto c_eq = eq(b);
-        s.add_clause(c_eq, ult(r, b), false);
-        s.add_clause(~c_eq, eq(q + 1), false);
+        s.add_clause("[axiom] quot_rem 4", {  c_eq, ult(r, b)  }, false);
+        s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1)  }, false);
 
         return {std::move(q), std::move(r)};
     }
@@ -523,9 +523,15 @@ namespace polysat {
     }
 
     pdd constraint_manager::bor(pdd const& p, pdd const& q) {
+#if 1
         // From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
         // found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
         return (p + q) - band(p, q);
+#else
+        // Alternatively, de Morgan:
+        // (advantage: only one occurrence of p, q)
+        return bnot(band(bnot(p), bnot(q)));
+#endif
     }
 
     pdd constraint_manager::bxor(pdd const& p, pdd const& q) {
diff --git a/src/math/polysat/log.cpp b/src/math/polysat/log.cpp
index 970ed5583..03113ddd2 100644
--- a/src/math/polysat/log.cpp
+++ b/src/math/polysat/log.cpp
@@ -25,7 +25,7 @@ Other:
 */
 
 /*
-  TODO: add "conditional" logs, i.e., the messages are held back and only printed when a non-conditional message is logged.
+  TODO: add deferred logs, i.e., the messages are held back and only printed when a non-conditional message is logged.
         Purpose: reduce noise, e.g., when printing prerequisites for transformations that do not always apply.
 */
 
diff --git a/src/math/polysat/log.h b/src/math/polysat/log.h
index e7720bb13..09db22813 100644
--- a/src/math/polysat/log.h
+++ b/src/math/polysat/log.h
@@ -114,7 +114,10 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 
 inline void set_log_enabled(bool) {}
 inline bool get_log_enabled() { return false; }
-class scoped_set_log_enabled {};
+class scoped_set_log_enabled {
+public:
+    scoped_set_log_enabled(bool) {}
+};
 
 #define LOG_(vlvl, lvl, x)  \
   do {                      \
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 621b7ebfd..f0c2e6dd7 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -45,6 +45,7 @@ namespace polysat {
         default:
             break;
         }
+        VERIFY(r.is_var());
     }
 
     lbool op_constraint::eval() const {
@@ -342,12 +343,12 @@ namespace polysat {
                 rational const& q_val = qv.val();
                 if (q_val >= N)
                     // q >= N ==> r = 0
-                    return s.mk_clause(~shl, ~s.ule(N, q()), s.eq(r()), true);
+                    return s.mk_clause("shl forward 1", {~shl, ~s.ule(N, q()), s.eq(r())}, true);
                 if (pv.is_val()) {
                     SASSERT(q_val.is_unsigned());
                     // p = p_val & q = q_val ==> r = p_val * 2^q_val
                     rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned());
-                    return s.mk_clause(~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true);
+                    return s.mk_clause("shl forward 2", {~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val)}, true);
                 }
             }
         }
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index 2a205aab7..5258c890c 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -27,21 +27,21 @@ namespace polysat {
     class op_constraint final : public constraint {
     public:
         enum class code {
-            /// r is the logical right shift of p by q
+            /// r is the logical right shift of p by q.
             lshr_op,
-            /// r is the arithmetic right shift of p by q
+            /// r is the arithmetic right shift of p by q.
             ashr_op,
-            /// r is the left shift of p by q
+            /// r is the left shift of p by q.
             shl_op,
-            /// r is the bit-wise 'and' of p and q
+            /// r is the bit-wise 'and' of p and q.
             and_op,
             /// r is the smallest multiplicative pseudo-inverse of p;
             /// by definition we set r == 0 when p == 0.
             /// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
             inv_op,
-            // r is the quotient of dividing p by q 
+            // r is the quotient of unsigned division of p by q.
             udiv_op,
-            // r is the remainder of dividing p by q
+            // r is the remainder of unsigned division of p by q.
             urem_op,
         };
     protected:
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 50222b7c7..db57cb09f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -934,9 +934,7 @@ namespace polysat {
         unsigned lvl = 0;
         for (signed_constraint c : m_viable.get_constraints(v)) {
             LOG("due to: " << lit_pp(*this, c));
-            if (!m_bvars.is_assigned(c.blit()))   // side condition, irrelevant because all vars are already in the main condition
-                continue;
-            SASSERT(m_bvars.is_assigned(c.blit()));
+            VERIFY(m_bvars.is_assigned(c.blit()));
             lvl = std::max(lvl, m_bvars.level(c.blit()));
             for (pvar w : c->vars())
                 if (is_assigned(w))  // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere.
@@ -1053,7 +1051,7 @@ namespace polysat {
         unsigned max_level = 0;             // highest level in lemma
         unsigned lits_at_max_level = 0;     // how many literals at the highest level in lemma
         unsigned snd_level = 0;             // second-highest level in lemma
-        unsigned num_undef = 0;        // whether there is an unassigned literal (at most one)
+        unsigned num_undef = 0;             // number of unassigned literals
         for (sat::literal lit : lemma) {
             switch (m_bvars.value(lit)) {
             case l_true:
@@ -1061,6 +1059,8 @@ namespace polysat {
             case l_false:
                 break;
             default:
+                // TODO: Entering this case means we used clause_builder::insert at some point where it should have been clause_builder::insert_eval?
+                //       Maybe we should just get rid of the insert/insert_eval distinction and evaluate everything here.
                 switch (lit2cnstr(lit).eval(*this)) {
                 case l_true:
                     return std::nullopt;
@@ -1069,15 +1069,11 @@ namespace polysat {
                     break;
                 case l_undef:
                     ++num_undef;
-                    // NSB: we used to not return null here.
-                    // Lemmas that were not false under evaluation are now skipped
-                    // with this change. 
                     if (num_undef > 1)
                         return std::nullopt;
                     continue;
                 }
             }
-
             unsigned const lit_level = m_bvars.level(lit);
             if (lit_level > max_level) {
                 snd_level = max_level;
@@ -1102,8 +1098,8 @@ namespace polysat {
         //                       backjump to max_level so we can propagate
         unsigned jump_level;
         unsigned branching_factor = lits_at_max_level;
-        if (num_undef == 1)
-            jump_level = max_level, branching_factor = 1;
+        if (num_undef >= 1)
+            jump_level = max_level, branching_factor = num_undef;
         else if (lits_at_max_level <= 1)
             jump_level = snd_level;
         else
@@ -1315,12 +1311,6 @@ namespace polysat {
         return lit;
     }
 
-    /**
-    * Activate constraint immediately
-    * Activation and de-activation of constraints follows the scope controlled by push/pop.
-    * constraints activated within the linear solver are de-activated when the linear
-    * solver is popped.
-    */
     void solver::activate_constraint(signed_constraint c) {
         SASSERT(c);
         LOG("Activating constraint: " << c);
@@ -1392,12 +1382,20 @@ namespace polysat {
             enqueue_pwatch(lit2cnstr(lit).get());
     }
 
-    void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
-        clause_ref clause = mk_clause(n, cs, is_redundant);
+    void solver::add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) {
+        clause_ref clause = mk_clause(name, n, cs, is_redundant);
         if (clause)
             add_clause(*clause);
     }
 
+    void solver::add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant) {
+        add_clause(name, static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
+    }
+
+    void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
+        add_clause("", n, cs, is_redundant);
+    }
+
     void solver::add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant) {
         add_clause(static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
     }
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 4dd49a945..83975ad01 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -327,6 +327,8 @@ namespace polysat {
         void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
         void add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant);
         void add_clause(unsigned n, signed_constraint const* cs, bool is_redundant);
+        void add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
+        void add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant);
 
         // Create a clause without adding it to the solver.
         clause_ref mk_clause(signed_constraint c1, bool is_redundant);
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index c7872798d..0258365dd 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -64,7 +64,9 @@ The following forms are equivalent:
 
 Useful lemmas:
 
-    - p <= q    ==>   p == 0  ||  -q <= -p
+    p <= q  &&  q+1 != 0    ==>  p+1 <= q+1
+
+    p <= q  &&  p != 0      ==>   -q <= -p
 
 --*/
 
@@ -104,19 +106,6 @@ namespace {
             return;
         }
 
-#if 0
-        // simple version that we had for a long time, subsumed by rule in #else
-
-        // p + 1 <= p  -->  p + 1 <= 0
-        // p <= p - 1  -->  p <= 0
-        //
-        // p + k <= p       -->  p + k <= k - 1
-        // p     <= p - k   -->  p     <= k - 1
-        if ((lhs - rhs).is_val()) {
-            pdd k = lhs - rhs;
-            rhs = k - 1;
-        }
-#else
         // Try to reduce the number of variables on one side using one of these rules:
         //
         //      p <= q  -->  p <= p - q - 1
@@ -144,11 +133,11 @@ namespace {
                 // verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
             }
         }
-#endif
 
 #if 0
-        // TODO: maybe enable this later to make some constraints more "readable"
+        // TODO: maybe enable this later to make some constraints more readable
         // p - k <= -k - 1  -->  k <= p
+        // ALTERNATIVE: p > k-1  to keep the polynomial on the lhs?  allows us to have boolean conflicts between x <= k and x > k ? (otherwise it is x <= k and k+1 <= x.)
         if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == (rhs + 1).val()) {
             // verbose_stream() << "IN:  " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
             std::abort();
@@ -172,16 +161,6 @@ namespace {
             is_positive = !is_positive;
         }
 
-#if 0
-        // TODO: enabling this rule leads to unsoundness in 1041-minimized (but the rule itself is correct)
-        // k <= p   -->   p - k <= - k - 1
-        if (lhs.is_val()) {
-            pdd k = lhs;
-            lhs = rhs - k;
-            rhs = - k - 1;
-        }
-#endif
-
         // p >  -2   -->   p + 1 <= 0
         // p <= -2   -->   p + 1 >  0
         if (rhs.is_val() && !rhs.is_zero() && (rhs + 2).is_zero()) {
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index af97ecb8d..85c8510a7 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -608,12 +608,12 @@ namespace {
         do {
             rational coeff_val = mod(e->coeff * val, mod_value);
             if (e->interval.currently_contains(coeff_val)) {
-                IF_LOGGING(
-                    verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
-                    for (const auto& src : e->src)
-                        verbose_stream() << lit_pp(s, src) << "\n";
-                );
-                LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << "    " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
+                // IF_LOGGING(
+                //     verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
+                //     for (const auto& src : e->src)
+                //         verbose_stream() << lit_pp(s, src) << "\n";
+                // );
+                // LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << "    " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
 
                 if (mod(e->interval.hi_val() + 1, mod_value) == e->interval.lo_val()) {
                     // We have an equation:  a * v == b
@@ -735,11 +735,12 @@ namespace {
         m_diseq_lin[v] = m_diseq_lin[v]->next();
 
         do {
-            IF_LOGGING(
-                    verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
-                    for (const auto& src : e->src)
-                        verbose_stream() << lit_pp(s, src) << "\n";
-            );
+            // IF_LOGGING(
+            //         verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
+            //         for (const auto& src : e->src)
+            //             verbose_stream() << lit_pp(s, src) << "\n";
+            // );
+
             // We compute an interval if the concrete value 'val' violates the constraint:
             //      p*val + q >  r*val + s  if e->src.is_positive()
             //      p*val + q >= r*val + s  if e->src.is_negative()
@@ -1907,8 +1908,7 @@ namespace {
 
     bool viable::resolve_interval(pvar v, conflict& core) {
         DEBUG_CODE( log(v); );
-        if (has_viable(v))
-            return false;
+        VERIFY(!has_viable(v));  // does a pass over interval refinement, making sure the intervals actually exist
 
 #if 0
         // Prefer bit information as justifications
@@ -1980,10 +1980,15 @@ namespace {
                 n = n1;
             }
 
-            // verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
-
             signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
-            lemma.insert_try_eval(~c);
+            // lemma.insert_try_eval(~c);
+            VERIFY(c.is_currently_true(s));
+            if (c.bvalue(s) == l_false) {
+                core.reset();
+                core.init(~c);
+                return false;
+            }
+            lemma.insert_eval(~c);
 
             for (auto sc : e->side_cond)
                 lemma.insert_eval(~sc);
@@ -1996,8 +2001,25 @@ namespace {
         }
         while (e != first);
 
-        // TODO: violated in bench27
-        SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
+        // TODO: violated in 5133-min.smt2:
+        //
+        //              viable lemma:
+        //             35: -31 <= -1*v17 + -1*v11*v0 + -1*v5*v2 + 32  [ b:l_true  p:l_false bprop@0 idx:28 pwatched ]
+        //            -22: v17 + v11*v0 + v6 + v5*v2 != 0  [ b:l_false p:l_undef assert@0 idx:8 pwatched dep:16 ]
+        //             36: v17 + v11*v0 + v5*v2 + 1 == 0   [ b:l_false p:l_false eval@39 idx:75 ]
+        //             -7: -31 > v6 + 32                   [ b:l_false p:l_undef assert@0 idx:17 pwatched dep:33 ]
+        //      ASSERTION VIOLATION
+        //      File: /Users/jakob/projects/z3/src/math/polysat/viable.cpp
+        //      Line: 2036
+        //      all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; })
+        //
+        //  Reason: there is an eval/bool conflict that we didn't discover before,
+        //          because not-yet-assigned variables are watched but the constraint already evaluates due to cancellation of some terms.
+        //
+        // verbose_stream() << "viable lemma:\n";
+        // for (auto lit : lemma)
+        //     verbose_stream() << "    " << lit_pp(s, lit) << "\n";
+        VERIFY(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
 
         core.add_lemma("viable", lemma.build());
         core.logger().log(inf_fi(*this, v));