From 3b0c8a7ff9068e128b39b8dc74e3c40f1e8e4547 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 28 May 2020 11:57:44 -0500 Subject: [PATCH] fix logic for disabling theory case split heuristic (#4397) --- src/smt/smt_context.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 617608d8e..4f90bbcef 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2939,12 +2939,14 @@ namespace smt { // If we don't use the theory case split heuristic, // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2) // to enforce the condition that at most one literal can be assigned 'true'. - if (!m_fparams.m_theory_case_split && !m.proofs_enabled()) { - for (unsigned i = 0; i < num_lits; ++i) { - for (unsigned j = i+1; j < num_lits; ++j) { - literal l1 = lits[i]; - literal l2 = lits[j]; - mk_clause(~l1, ~l2, (justification*) nullptr); + if (!m_fparams.m_theory_case_split) { + if (!m.proofs_enabled()) { + for (unsigned i = 0; i < num_lits; ++i) { + for (unsigned j = i + 1; j < num_lits; ++j) { + literal l1 = lits[i]; + literal l2 = lits[j]; + mk_clause(~l1, ~l2, (justification*) nullptr); + } } } } else {