Skip to content

Commit b44c897

Browse files
authored
Fix setup_relevancy for relevancy-dependent case split strategies (#7662)
1 parent 80c553d commit b44c897

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

src/smt/smt_setup.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -834,6 +834,13 @@ namespace smt {
834834
// there are some other cases where relevancy propagation is harmful.
835835
//
836836
void setup::setup_relevancy(static_features& st) {
837+
// the case split queue has been constructed by now.
838+
// it is not safe to disable relevancy if the case split stragegy is relevancy-dependent.
839+
if (m_params.m_case_split_strategy == CS_RELEVANCY ||
840+
m_params.m_case_split_strategy == CS_RELEVANCY_ACTIVITY ||
841+
m_params.m_case_split_strategy == CS_RELEVANCY_GOAL)
842+
return;
843+
837844
if (st.m_has_bv && !st.m_has_fpa && st.m_num_quantifiers == 0)
838845
m_params.m_relevancy_lvl = 0;
839846
}

0 commit comments

Comments
 (0)