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

Fixed missing assignment for binary clauses (#6148)

Browse source 
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int

* Fixed missing assignment for binary clauses
This commit is contained in:
Clemens Eisenhofer 2022-07-11 18:24:03 +02:00 committed by GitHub
parent 9d9414c111
commit 1f2346073a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_internalizer.cpp
View file

@ -1429,7 +1429,10 @@ namespace smt {
inc_ref(l2); inc_ref(l2);
m_watches[(~l1).index()].insert_literal(l2); m_watches[(~l1).index()].insert_literal(l2);
m_watches[(~l2).index()].insert_literal(l1); 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)); assign(l1, b_justification(~l2));
} }
m_clause_proof.add(l1, l2, k, j); m_clause_proof.add(l1, l2, k, j);