mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #1571

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-12 15:59:06 +08:00
parent f77cfc1487
commit 28fbcd7687
1 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_pb.cpp
View file

@ -446,7 +446,16 @@ namespace smt {
expr* arg = atom->get_arg(i); expr* arg = atom->get_arg(i);
literal l = compile_arg(arg); literal l = compile_arg(arg);
numeral c = m_util.get_coeff(atom, i); numeral c = m_util.get_coeff(atom, i);
args.push_back(std::make_pair(l, c)); switch (ctx.get_assignment(l)) {
case l_true:
k -= c;
break;
case l_false:
break;
default:
args.push_back(std::make_pair(l, c));
break;
}
} }
if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) { if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) {
// turn W <= k into -W >= -k // turn W <= k into -W >= -k
@ -458,7 +467,7 @@ namespace smt {
else { else {
SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom) || m_util.is_eq(atom)); SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom) || m_util.is_eq(atom));
} }
TRACE("pb", display(tout, *c);); TRACE("pb", display(tout, *c, true););
//app_ref fml1(m), fml2(m); //app_ref fml1(m), fml2(m);
//fml1 = c->to_expr(ctx, m); //fml1 = c->to_expr(ctx, m);
c->unique(); c->unique();