From 6b319f9ac323d3a0f79e1217a4b1385fcbb47722 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 11:49:05 -0700 Subject: [PATCH] fix #3297 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 10fb7836e..489a1c607 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2981,7 +2981,7 @@ 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) { + 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];