mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 23:05:26 +00:00
Code Activity

revert assumption tracking choice in unit literals inferred from binary clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-12 11:08:35 -08:00
parent e4d6aa07dc
commit f835a3c2b2
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver.cpp
View file

@ -344,11 +344,11 @@ namespace sat {
void solver::mk_bin_clause(literal l1, literal l2, bool learned) { void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
if (find_binary_watch(get_wlist(~l1), ~l2)) { if (find_binary_watch(get_wlist(~l1), ~l2)) {
assign_core(l1, 0, justification(l1)); assign_core(l1, 0, justification(l2));
return; return;
} }
if (find_binary_watch(get_wlist(~l2), ~l1)) { if (find_binary_watch(get_wlist(~l2), ~l1)) {
assign_core(l2, 0, justification(l2)); assign_core(l2, 0, justification(l1));
return; return;
} }
watched* w0 = find_binary_watch(get_wlist(~l1), l2); watched* w0 = find_binary_watch(get_wlist(~l1), l2);