mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 11:51:20 +00:00
Code Activity

investigating conflict resolution bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-08 21:40:53 -08:00
parent 0f0397b05f
commit ec84d69206
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_b_justification.h
View file

@ -54,7 +54,7 @@ namespace smt {
m_data(BOXTAGINT(void*, l.index(), BIN_CLAUSE)) { m_data(BOXTAGINT(void*, l.index(), BIN_CLAUSE)) {
} }
explicit b_justification(justification * js): explicit b_justification(justification * js):
m_data(TAG(void*, js, JUSTIFICATION)) { m_data(TAG(void*, js, JUSTIFICATION)) {
SASSERT(js); SASSERT(js);
} }

14
src/smt/theory_pb.cpp
View file

@ -1211,7 +1211,7 @@ namespace smt {
while (m_num_marks > 0) { while (m_num_marks > 0) {
m_lemma.normalize(); //m_lemma.normalize();
SASSERT(m_lemma.well_formed()); SASSERT(m_lemma.well_formed());
// //
@ -1222,7 +1222,11 @@ namespace smt {
v = conseq.var(); v = conseq.var();
--idx; --idx;
} }
while (!is_marked(v)); while (!is_marked(v) && idx > 0);
if (idx == 0) {
IF_VERBOSE(1, verbose_stream() << "BUG?!\n";);
return false;
}
unsigned conseq_index = m_conseq_index[v]; unsigned conseq_index = m_conseq_index[v];
numeral conseq_coeff = m_lemma.coeff(conseq_index); numeral conseq_coeff = m_lemma.coeff(conseq_index);
@ -1254,7 +1258,7 @@ namespace smt {
clause& cls = *js.get_clause(); clause& cls = *js.get_clause();
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(1, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";);
m_ineq_literals.push_back(conseq); m_ineq_literals.push_back(conseq);
break; break;
} }
@ -1286,8 +1290,8 @@ namespace smt {
justification& j = *js.get_justification(); justification& j = *js.get_justification();
// 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 theory " << conseq << "\n";); IF_VERBOSE(1, verbose_stream() << "skipping justification for " << conseq
IF_VERBOSE(0, verbose_stream() << j.get_from_theory() << "\n";); << " from theory " << j.get_from_theory() << "\n";);
m_ineq_literals.push_back(conseq); m_ineq_literals.push_back(conseq);
break; break;
} }