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

add back skipped consequences, exposed by fu-malik assertion violation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-04 13:11:58 -08:00
parent b980a15177
commit ead414c4ee
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_pb.cpp
View file

@ -1251,6 +1251,7 @@ namespace smt {
justification* cjs = cls.get_justification(); justification* cjs = cls.get_justification();
if (cjs) { if (cjs) {
IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";); IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";);
m_ineq_literals.push_back(conseq);
break; break;
} }
unsigned num_lits = cls.get_num_literals(); unsigned num_lits = cls.get_num_literals();
@ -1282,6 +1283,7 @@ namespace smt {
// only process pb justifications. // only process pb justifications.
if (j.get_from_theory() != get_id()) { if (j.get_from_theory() != get_id()) {
IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";); IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";);
m_ineq_literals.push_back(conseq);
break; break;
} }
pb_justification& pbj = dynamic_cast<pb_justification&>(j); pb_justification& pbj = dynamic_cast<pb_justification&>(j);