From 8f3e8bd0bb2a31a9d971f81ed6ae72ca85f90ba4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Jan 2024 10:37:55 -0800
Subject: [PATCH] create proper extract terms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_bv_plugin.cpp |  4 +++-
 src/ast/euf/euf_egraph.cpp    | 14 +++++++-------
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 4a2b2e12b..4fc9c09f3 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -171,7 +171,9 @@ namespace euf {
 
             if (is_extract(p, lo, hi)) {
                 auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
-                push_merge(mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p)));
+                auto ix = x->get_interpreted();
+                auto ex = mk(bv.mk_extract(hi, lo, ix->get_expr()), 1, &ix);
+                push_merge(ex, mk_value(val_p, width(p)));
             }
         }
 
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 0c24287ef..f19a146c5 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -69,7 +69,7 @@ namespace euf {
     }
 
     enode_bool_pair egraph::insert_table(enode* p) {
-        TRACE("euf", tout << "insert_table " << bpp(p) << "\n");
+        TRACE("euf_verbose", tout << "insert_table " << bpp(p) << "\n");
         //SASSERT(!m_table.contains_ptr(p));
         auto rc = m_table.insert(p);
         p->m_cg = rc.first;
@@ -522,7 +522,7 @@ namespace euf {
     }
 
     void egraph::remove_parents(enode* r) {
-        TRACE("euf", tout << bpp(r) << "\n");
+        TRACE("euf_verbose", tout << bpp(r) << "\n");
         SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
         for (enode* p : enode_parents(r)) {
             if (p->is_marked1())
@@ -533,7 +533,7 @@ namespace euf {
                 SASSERT(m_table.contains_ptr(p));
                 p->mark1();
                 erase_from_table(p);
-                CTRACE("euf", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
+                CTRACE("euf_verbose", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
                 SASSERT(!m_table.contains_ptr(p));
             }
             else if (p->is_equality())
@@ -546,11 +546,11 @@ namespace euf {
             if (!p->is_marked1())
                 continue;
             p->unmark1();
-            TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
+            TRACE("euf_verbose", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
             if (p->cgc_enabled()) {
                 auto [p_other, comm] = insert_table(p);
                 SASSERT(m_table.contains_ptr(p) == (p_other == p));
-                CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
+                CTRACE("euf_verbose", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
                 if (p_other != p) 
                     m_to_merge.push_back(to_merge(p_other, p, comm));                
                 else
@@ -584,14 +584,14 @@ namespace euf {
 
     void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
         enode* r2 = r1->get_root();
-        TRACE("euf", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
+        TRACE("euf_verbose", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
         r2->dec_class_size(r1->class_size());
         r2->set_is_shared(l_undef);
         std::swap(r1->m_next, r2->m_next);
         auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents();
         for (auto it = begin; it != end; ++it) {
             enode* p = *it;
-            TRACE("euf", tout << "erase " << bpp(p) << "\n";);
+            TRACE("euf_verbose", tout << "erase " << bpp(p) << "\n";);
             SASSERT(!p->cgc_enabled() || m_table.contains_ptr(p));
             SASSERT(!p->cgc_enabled() || p->is_cgr());
             if (p->cgc_enabled())