From ae18150d874f43b99fa1761b2013dd3784326299 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 14 May 2020 12:51:20 -0400 Subject: [PATCH] ignore true/false/null literals during theory case split propagation --- src/smt/smt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5fb36a28b..709dabd09 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3018,7 +3018,8 @@ namespace smt { literal l2 = *set_it; if (l2 != l) { b_justification js(l); - TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.c_ptr());); + TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.c_ptr()); tout << std::endl;); + if (l2 == true_literal || l2 == false_literal || l2 == null_literal) continue; assign(~l2, js); if (inconsistent()) { TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);