From b44c897a59bab4b7abb465a00fa097782c82545a Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 27 May 2025 17:52:35 +0200 Subject: [PATCH] Fix setup_relevancy for relevancy-dependent case split strategies (#7662) --- src/smt/smt_setup.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 384c4d850..4aad75833 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -834,6 +834,13 @@ namespace smt { // there are some other cases where relevancy propagation is harmful. // void setup::setup_relevancy(static_features& st) { + // the case split queue has been constructed by now. + // it is not safe to disable relevancy if the case split stragegy is relevancy-dependent. + if (m_params.m_case_split_strategy == CS_RELEVANCY || + m_params.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || + m_params.m_case_split_strategy == CS_RELEVANCY_GOAL) + return; + if (st.m_has_bv && !st.m_has_fpa && st.m_num_quantifiers == 0) m_params.m_relevancy_lvl = 0; }