From 333b32b0d2c829e771f2e9c9d632f00632220b44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jun 2019 16:32:45 +0200 Subject: [PATCH] disable adding redundant ite clauses as lemma. Add as non-redundant Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index c38e7020c..a53ed94a8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -337,8 +337,8 @@ struct goal2sat::imp { mk_clause(l, ~c, ~t); mk_clause(l, c, ~e); if (m_ite_extra) { - mk_clause(~t, ~e, l, true); - mk_clause(t, e, ~l, true); + mk_clause(~t, ~e, l, false); + mk_clause(t, e, ~l, false); } m_result_stack.shrink(sz-3); if (sign)