From f835a3c2b2a959abeca4d4e1b9e19e6d8e31405b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Jan 2019 11:08:35 -0800 Subject: [PATCH] revert assumption tracking choice in unit literals inferred from binary clauses 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 43adebb25..c9b535997 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -344,11 +344,11 @@ namespace sat { void solver::mk_bin_clause(literal l1, literal l2, bool learned) { if (find_binary_watch(get_wlist(~l1), ~l2)) { - assign_core(l1, 0, justification(l1)); + assign_core(l1, 0, justification(l2)); return; } if (find_binary_watch(get_wlist(~l2), ~l1)) { - assign_core(l2, 0, justification(l2)); + assign_core(l2, 0, justification(l1)); return; } watched* w0 = find_binary_watch(get_wlist(~l1), l2);