From 489a1495d2e6dbae5e7436ebb7d96527a0eaf300 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 19 Mar 2024 14:23:44 +0100
Subject: [PATCH] dep

---
 src/sat/smt/polysat_egraph.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index 3c0ee0fe0..cd48db612 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -138,11 +138,12 @@ namespace polysat {
             rational value;
             VERIFY(bv.is_numeral(r->get_expr(), value));
 
-            unsigned level = merge_level(n, r);
+            unsigned level = merge_level(n, r);  // TODO: WRONG -- n is not actually guaranteed to be the subslice of pv
 
             euf::theory_var u = n->get_th_var(get_id());
             // dependency dep = (u == euf::null_theory_var || u == w) ? dependency::axiom() : dependency(u, w);   // TODO: probably need an enode_pair instead?
-            dependency dep = dependency(n, r);
+            // dependency dep = dependency(n, r);
+            dependency dep = fixed_claim(pv, null_var, value, offset, length);
 
 #if GET_FIXED_SUB_SLICES_DISPLAY
             verbose_stream() << "    " << value << "[" << length << "]@" << offset;