From b86d472eaf5767cc2d870a08d0c22b70b2262f47 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 18:22:49 -0400 Subject: [PATCH] simplify theory case split handling --- src/smt/smt_context.cpp | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9a841ea26..af45f0fcc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3057,19 +3057,8 @@ namespace smt { literal l2 = *set_it; if (l2 != l) { b_justification js(l); - switch (get_assignment(l2)) { - case l_false: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;); - break; - case l_undef: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;); - assign(~l2, js); - break; - case l_true: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;); - assign(~l2, js); - break; - } + TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr());); + assign(~l2, js); if (inconsistent()) { TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); return false;