Merge pull request #4325 from mtrberzi/issue4322

ignore true/false/null literals during theory case split propagation
Z3Prover · May 16, 2020 · ce07138 · ce07138
2 parents fcbcad6 + ae18150
commit ce07138
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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;);