From a74ac93bcc3dfec5429861fef95eafeac439f03a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Mar 2019 13:34:31 -0700 Subject: [PATCH] fix #2196 Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 19e7d6ba2..b329cb06e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -549,9 +549,14 @@ struct goal2sat::imp { SASSERT(k.is_unsigned()); sat::literal_vector lits; convert_pb_args(t->get_num_args(), lits); + unsigned k2 = k.get_unsigned(); if (root && m_solver.num_user_scopes() == 0) { m_result_stack.reset(); - m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned()); + if (sign) { + for (sat::literal& l : lits) l.neg(); + k2 = lits.size() + 1 - k2; + } + m_ext->add_at_least(sat::null_bool_var, lits, k2); } else { sat::bool_var v = m_solver.add_var(true); @@ -571,14 +576,19 @@ struct goal2sat::imp { for (sat::literal& l : lits) { l.neg(); } + unsigned k2 = lits.size() - k.get_unsigned(); if (root && m_solver.num_user_scopes() == 0) { m_result_stack.reset(); - m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned()); + if (sign) { + for (sat::literal& l : lits) l.neg(); + k2 = lits.size() + 1 - k2; + } + m_ext->add_at_least(sat::null_bool_var, lits, k2); } else { sat::bool_var v = m_solver.add_var(true); sat::literal lit(v, false); - m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); + m_ext->add_at_least(v, lits, k2); m_cache.insert(t, lit); if (sign) lit.neg(); push_result(root, lit, t->get_num_args());