mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix #2196

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-22 13:34:31 -07:00
parent eae4fd6afd
commit a74ac93bcc
1 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/sat/tactic/goal2sat.cpp
View file

@ -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());