mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
Merge pull request #4325 from mtrberzi/issue4322
ignore true/false/null literals during theory case split propagation
This commit is contained in:
commit
ce07138008
|
@ -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;);
|
||||
|
|
Loading…
Reference in a new issue