mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

don't assign already assigned literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-16 11:41:32 -08:00
parent e94aa5bb1d
commit 247980c5a2
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

@ -348,11 +348,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) && value(l1) == l_undef) {
assign_core(l1, 0, justification(l2)); assign_core(l1, 0, justification(l2));
return; return;
} }
if (find_binary_watch(get_wlist(~l2), ~l1)) { if (find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
assign_core(l2, 0, justification(l1)); assign_core(l2, 0, justification(l1));
return; return;
} }