Fixed missing assignment for binary clauses (#6148)

* Added function to select the next variable to split on * Fixed typo * Small fixes * uint -> int * Fixed missing assignment for binary clauses
Z3Prover · Jul 11, 2022 · 1f23460 · 1f23460
1 parent 9d9414c
commit 1f23460
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
@@ -1429,7 +1429,10 @@ namespace smt {
                 inc_ref(l2);
                 m_watches[(~l1).index()].insert_literal(l2);
                 m_watches[(~l2).index()].insert_literal(l1);
-                if (get_assignment(l2) == l_false) {
+                if (get_assignment(l1) == l_false) {
+                    assign(l2, b_justification(~l1));
+                }
+                else if (get_assignment(l2) == l_false) {
                     assign(l1, b_justification(~l2));
                 }
                 m_clause_proof.add(l1, l2, k, j);