mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix bug in conflict resoltion tracking decision variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-03 21:10:54 -08:00
parent e3fe80fd4d
commit b9d433e3e5
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_pb.cpp
View file

@ -616,7 +616,7 @@ namespace smt {
}
TRACE("pb",
tout << "assign: " << c.lit() << " <- " << is_true << "\n";
tout << "assign: " << c.lit() << "\n";
display(tout, c); );
if (maxsum < c.k()) {
@ -1243,6 +1243,10 @@ namespace smt {
TRACE("pb", tout << "binary: " << js.get_literal() << "\n";);
break;
case b_justification::AXIOM:
if (ctx.get_assign_level(v) > ctx.get_base_level()) {
m_ineq_literals.push_back(conseq);
}
TRACE("pb", tout << "axiom " << conseq << "\n";);
break;
case b_justification::JUSTIFICATION: {
justification& j = *js.get_justification();
@ -1267,7 +1271,11 @@ namespace smt {
unset_mark(m_lemma.lit(i));
}
TRACE("pb", display(tout << "lemma: ", m_lemma););
TRACE("pb",
for (unsigned i = 0; i < m_ineq_literals.size(); ++i) {
tout << m_ineq_literals[i] << " ";
}
display(tout << "=> ", m_lemma););
hoist_maximal_values();