From 100253856584de5d019eb917363232ebdb2bb6ba Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 5 Jan 2023 17:41:08 +0100
Subject: [PATCH] insert_eval?

---
 src/math/polysat/solver.cpp               | 4 ++++
 src/math/polysat/variable_elimination.cpp | 6 +++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index a00f6a831..b615e6d20 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -904,6 +904,10 @@ namespace polysat {
             if (m_bvars.is_true(lit))  // may happen if we only use the clause to justify a new constraint; it is not a real lemma
                 return std::nullopt;
             if (!m_bvars.is_assigned(lit)) {
+                DEBUG_CODE({
+                    if (lit2cnstr(lit).eval(*this) != l_undef)
+                        LOG("WARNING: missed evaluation of literal: " << lit_pp(*this, lit));
+                });
                 SASSERT(!is_propagation);
                 is_propagation = true;
                 continue;
diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index b4381b44d..eeba1d6cf 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -697,15 +697,15 @@ namespace polysat {
         pdd a_pi = get_pseudo_inverse(a, a_parity);
 #else
         pdd a_pi = s.pseudo_inv(a);
-        //precondition.insert(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
-        precondition.insert(~s.parity_at_most(a, a_parity));
+        //precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
+        precondition.insert_eval(~s.parity_at_most(a, a_parity));
 #endif
         
         pdd shift = a;
         
         if (a_parity > 0) {
             shift = s.lshr(a1, a1.manager().mk_val(a_parity));
-            precondition.insert(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
+            precondition.insert_eval(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
         }
         LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
         LOG("a: " << a);