From d889fcdca6432db36684a9de23626a659f7f5a8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2017 19:26:54 -0800 Subject: [PATCH] fix translation of <= 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 41fb4dfce..eb90edd3d 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -420,7 +420,7 @@ struct goal2sat::imp { lits[i].neg(); } sat::bool_var v = m_solver.mk_var(true); - m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned() + 1); + m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); if (root) { m_result_stack.reset(); mk_clause(sat::literal(v, sign)); @@ -442,7 +442,7 @@ struct goal2sat::imp { for (unsigned i = 0; i < lits.size(); ++i) { lits[i].neg(); } - m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned() + 1); + m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned()); if (root) { m_result_stack.reset(); if (sign) {