From 247980c5a28e44ff367ce9a3dbbcfc6a85d73d66 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Jan 2019 11:41:32 -0800 Subject: [PATCH] don't assign already assigned literals Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5fdd05884..3c97a985f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -348,11 +348,11 @@ namespace sat { } 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)); 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)); return; }