fix #4909

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 20, 2020 · cd77a4d · cd77a4d
1 parent 8e0a2c9
commit cd77a4d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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);