From 8c5abdf818ebd674d57a8dc43f3fe04d73f6ab73 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Jan 2025 08:14:53 -0800
Subject: [PATCH] Can's fix to relevancy propagation

---
 src/smt/dyn_ack.cpp     | 6 ++++++
 src/smt/smt_context.cpp | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 66a2c2d5d..6ac67663a 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -425,6 +425,9 @@ namespace smt {
         lits.push_back(mk_eq(n1, n2));
         clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
 
+        for (auto lit : lits) 
+            m_context.mark_as_relevant(lit);        
+
         justification * js = nullptr;
         if (m.proofs_enabled())
             js = alloc(dyn_ack_cc_justification, n1, n2);
@@ -484,6 +487,9 @@ namespace smt {
                        m.mk_eq(n2, r),
                        m.mk_eq(n1, n2));
         }
+        ctx.mark_as_relevant(eq1);
+        ctx.mark_as_relevant(eq2);
+        ctx.mark_as_relevant(eq3);
         clause * cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 96b66149a..153dcae18 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2321,6 +2321,8 @@ namespace smt {
                         });
                         literal l(v, sign);
                         cls->set_literal(j, l);
+                        if (cls->get_kind() == CLS_TH_LEMMA)
+                            mark_as_relevant(l);
                     }
                     SASSERT(ilvl <= m_scope_lvl);
                     int w1_idx = select_watch_lit(cls, 0);
@@ -2349,6 +2351,10 @@ namespace smt {
                     SASSERT(!cls->reinternalize_atoms());
                     literal l1 = cls->get_literal(0);
                     literal l2 = cls->get_literal(1);
+                    if (cls->get_kind() == CLS_TH_LEMMA) {
+                        mark_as_relevant(l1);
+                        mark_as_relevant(l2);
+                    }
                     if (get_assignment(l1) == l_false && is_empty_clause(cls)) {
                         set_conflict(b_justification(cls));
                         keep = true;