From ec84d69206e61adbd227dd8e5634e0cd359aca2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Dec 2013 21:40:53 -0800 Subject: [PATCH] investigating conflict resolution bug Signed-off-by: Nikolaj Bjorner --- src/smt/smt_b_justification.h | 2 +- src/smt/theory_pb.cpp | 14 +++++++++----- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_b_justification.h b/src/smt/smt_b_justification.h index 4798af4b0..5a82e36e8 100644 --- a/src/smt/smt_b_justification.h +++ b/src/smt/smt_b_justification.h @@ -54,7 +54,7 @@ namespace smt { m_data(BOXTAGINT(void*, l.index(), BIN_CLAUSE)) { } - explicit b_justification(justification * js): + explicit b_justification(justification * js): m_data(TAG(void*, js, JUSTIFICATION)) { SASSERT(js); } diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index eecb1109b..355e9a3d5 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1211,7 +1211,7 @@ namespace smt { while (m_num_marks > 0) { - m_lemma.normalize(); + //m_lemma.normalize(); SASSERT(m_lemma.well_formed()); // @@ -1222,7 +1222,11 @@ namespace smt { v = conseq.var(); --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]; numeral conseq_coeff = m_lemma.coeff(conseq_index); @@ -1254,7 +1258,7 @@ namespace smt { clause& cls = *js.get_clause(); justification* cjs = cls.get_justification(); 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); break; } @@ -1286,8 +1290,8 @@ namespace smt { justification& j = *js.get_justification(); // only process pb justifications. if (j.get_from_theory() != get_id()) { - IF_VERBOSE(0, verbose_stream() << "skipping justification for theory " << conseq << "\n";); - IF_VERBOSE(0, verbose_stream() << j.get_from_theory() << "\n";); + IF_VERBOSE(1, verbose_stream() << "skipping justification for " << conseq + << " from theory " << j.get_from_theory() << "\n";); m_ineq_literals.push_back(conseq); break; }