From fd9c931168bcb5bf9d868892dfdbd9ae45bc43a0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 20 Mar 2024 15:37:03 +0100
Subject: [PATCH] skip entry for origin variable

---
 src/sat/smt/polysat/project_interval.cpp | 1 +
 src/sat/smt/polysat_egraph.cpp           | 5 ++++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/polysat/project_interval.cpp b/src/sat/smt/polysat/project_interval.cpp
index 5b8ce9d2e..635cdff75 100644
--- a/src/sat/smt/polysat/project_interval.cpp
+++ b/src/sat/smt/polysat/project_interval.cpp
@@ -179,6 +179,7 @@ namespace polysat {
     lbool project_interval::try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& value, unsigned const max_level) {
         SASSERT(w != null_var);
         SASSERT_EQ(c.size(w), w_sz);
+        SASSERT(w != m_var);
         if (w == m_var)
             return l_undef;
 
diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index 3c20c79aa..8648df4d3 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -125,7 +125,8 @@ namespace polysat {
 
     // walk the e-graph to retrieve fixed sub-slices along with justifications,
     // as well as pvars that correspond to these sub-slices.
-    void solver::get_fixed_sub_slices(pvar pv, fixed_bits_vector& fixed) {
+    // does not retrieve a slice corresponding to 'pv' itself.
+    void solver::get_fixed_sub_slices(pvar const pv, fixed_bits_vector& fixed) {
         #define GET_FIXED_SUB_SLICES_DISPLAY 1
         auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
             euf::enode* r = n->get_root();
@@ -180,6 +181,8 @@ namespace polysat {
                 auto const& p = m_var2pdd[s];
                 if (!p.is_var())
                     continue;
+                if (p.var() == pv)
+                    continue;
                 // unsigned p_level = merge_level(sib, r);  // this is ok
 #if GET_FIXED_SUB_SLICES_DISPLAY
                 verbose_stream() << "        pvar " << p;