mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

ignore true/false/null literals during theory case split propagation

Browse source
This commit is contained in:
Murphy Berzish 2020-05-14 12:51:20 -04:00
parent 73fa5995d4
commit ae18150d87
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.cpp
View file

@ -3018,7 +3018,8 @@ namespace smt {
literal l2 = *set_it; literal l2 = *set_it;
if (l2 != l) { if (l2 != l) {
b_justification js(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); assign(~l2, js);
if (inconsistent()) { if (inconsistent()) {
TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);