From e978b81c7a43eae5de453bb0f7af1790bbe01293 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Dec 2022 12:40:47 -0800
Subject: [PATCH] add review comment to bug location

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/saturation.cpp | 9 ++++++---
 src/math/polysat/solver.cpp     | 2 ++
 src/math/polysat/viable.cpp     | 7 +++++++
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index ab999fe7b..cc89073f8 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1199,7 +1199,6 @@ namespace polysat {
     bool saturation::try_factor_equality2(pvar x, conflict& core, inequality const& a_l_b) {
         set_rule("[x] ax + b = 0 & C[x] => C[-inv(a)*b]");
         auto& m = s.var2pdd(x);       
-        unsigned N = m.power_of_2();
         pdd y  = m.zero();
         pdd a = y, b = y, a1 = y, b1 = y;        
         if (!is_AxB_eq_0(x, a_l_b, a, b, y))
@@ -1242,20 +1241,24 @@ namespace polysat {
                 auto const& ule = c->to_ule();
                 auto p = replace(ule.lhs());
                 auto q = replace(ule.rhs());
+                if (!change)
+                    continue;
                 m_lemma.reset();
                 m_lemma.insert(~c);
                 m_lemma.insert_eval(~s.eq(y));
-                if (change && propagate(x, core, a_l_b, c.is_positive() ? s.ule(p, q) : ~s.ule(p, q)))
+                if (propagate(x, core, a_l_b, c.is_positive() ? s.ule(p, q) : ~s.ule(p, q)))
                     prop = true;
             }
             else if (c->is_umul_ovfl()) {
                 auto const& ovf = c->to_umul_ovfl();
                 auto p = replace(ovf.p());
                 auto q = replace(ovf.q());
+                if (!change)
+                    continue;
                 m_lemma.reset();
                 m_lemma.insert(~c);
                 m_lemma.insert_eval(~s.eq(y));
-                if (change && propagate(x, core, a_l_b, c.is_positive() ? s.umul_ovfl(p, q) : ~s.umul_ovfl(p, q)))
+                if (propagate(x, core, a_l_b, c.is_positive() ? s.umul_ovfl(p, q) : ~s.umul_ovfl(p, q)))
                     prop = true;
             }
         }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0d2c2a96d..bdc2b3f8c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1060,6 +1060,8 @@ namespace polysat {
     void solver::assign_eval(sat::literal lit) {
         signed_constraint const c = lit2cnstr(lit);
         LOG_V(10, "Evaluate: " << lit_pp(*this ,lit));
+        // assertion is false
+        if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n");
         SASSERT(c.is_currently_true(*this));
         VERIFY(c.is_currently_true(*this));
         unsigned level = 0;
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index e51a80bb9..2e05c5b1d 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -169,6 +169,13 @@ namespace polysat {
         //       - side conditions
         //       - i.lo() == i.lo_val() for each unit interval i
         //       - i.hi() == i.hi_val() for each unit interval i
+
+        // NSB review:
+        // the bounds added by x < p and p < x in forbidden_intervals
+        // match_non_max
+        // use values that are approximations. Then the propagations in
+        // try_assign_eval are incorrect.
+        
         for (auto const& c : get_constraints(v)) {
             s.try_assign_eval(c);
         }