From 1f0a6c051ab6a90df86c3dabfbf9159ccbc97c05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Mar 2024 11:49:11 -0700 Subject: [PATCH] update slice/offset claim structures to allow for equal variable. Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat_egraph.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index e1489bef2..b8351fe14 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -204,8 +204,7 @@ namespace polysat { if (slice.child != null_var) { auto c = var2enode(m_pddvar2var[slice.child]); - if (b != c) - m_bv_plugin->explain_slice(b, 0, c, consume_eq); + m_bv_plugin->explain_slice(b, 0, c, consume_eq); } }