From cd77a4d9a5e31b839faa66a51415980aae7b75c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Dec 2020 11:53:19 -0800 Subject: [PATCH] fix #4909 Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 88e343d9f..bfcf7ff0f 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -566,12 +566,12 @@ struct goal2sat::imp : public sat::sat_internalizer { else { sat::bool_var k = add_var(false, t); sat::literal l(k, false); - m_cache.insert(t, l); mk_clause(~l, l1, ~l2); mk_clause(~l, ~l1, l2); mk_clause(l, l1, l2); mk_clause(l, ~l1, ~l2); if (aig()) aig()->add_iff(l, l1, l2); + m_cache.insert(t, m.is_xor(t) ? ~l : l); if (sign) l.neg(); m_result_stack.push_back(l);