From 9fb2b491d6f5108494df2e17609409bfa448b775 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 15:17:14 -0700 Subject: [PATCH] remove relvancy marking code Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9664dd73e..0248c75a6 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1786,8 +1786,8 @@ namespace smt { // if the instantiation creates a conflict, we backtrack immediately. // to retain the conflict clause being relevant we mark it here. // if the instantiation does not create a conflict, default relevancy propagation applies. - if (inconsistent()) - mark_as_relevant(body); + //if (inconsistent() && is_app(body)) + // for (auto arg: *to_app(body)) mark_as_relevant(arg); m_case_split_queue->internalize_instance_eh(body, generation); }