fix #7098

Z3Prover · Jan 31, 2024 · 50deece · 50deece
1 parent 99ebbd6
commit 50deece
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 12 deletions.
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
@@ -132,7 +132,7 @@ namespace smt {
 
     void context::display_literal_info(std::ostream & out, literal l) const {
         smt::display_compact(out, l, m_bool_var2expr.data());
-        display_literal_smt2(out, l);
+        display_literal_smt2(out << " " << l << ": ", l);
         out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
     }
 

diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
@@ -1807,7 +1807,7 @@ namespace smt {
 
     bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) {
 
-        TRACE("pb", display(tout, c, true); );
+        TRACE("pb", display(tout << "resolve conflict\n", c, true); );
 
         bool_var v;
         m_conflict_lvl = 0;
@@ -1839,8 +1839,19 @@ namespace smt {
         literal conseq = ~confl[2];
         int bound = 1;
 
+        auto clear_marks = [&]() {
+            while (m_num_marks > 0 && idx > 0) {
+                v = lits[idx].var();
+                if (ctx.is_marked(v)) {
+                    ctx.unset_mark(v);
+                }
+                --idx;
+            }
+        };
+
         while (m_num_marks > 0) {
 
+            TRACE("pb", tout << "conseq: " << conseq << "\n");
             v = conseq.var();
 
             int offset = get_abs_coeff(v);
@@ -1850,13 +1861,7 @@ namespace smt {
             }
             SASSERT(validate_lemma());
             if (offset > 1000) {
-                while (m_num_marks > 0 && idx > 0) {
-                    v = lits[idx].var();
-                    if (ctx.is_marked(v)) {
-                        ctx.unset_mark(v);
-                    }
-                    --idx;
-                }
+                clear_marks();
                 return false;
             }
 
@@ -1884,8 +1889,11 @@ namespace smt {
                 clause& cls = *js.get_clause();
                 justification* cjs = cls.get_justification();
                 unsigned num_lits = cls.get_num_literals();
-                if (cjs && typeid(smt::unit_resolution_justification) == typeid(*cjs))
-                    ;
+                CTRACE("pb", cjs, tout << (typeid(smt::unit_resolution_justification) == typeid(*cjs)) << "\n");
+                if (cjs && typeid(smt::unit_resolution_justification) == typeid(*cjs)) {
+                    clear_marks();
+                    return false;
+                }
                 else if (cjs && !is_proof_justification(*cjs)) {                    
                     TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";);
                     break;
@@ -1954,7 +1962,8 @@ namespace smt {
             while (true) {
                 conseq = lits[idx];
                 v = conseq.var();
-                if (ctx.is_marked(v)) break;
+                if (ctx.is_marked(v))
+                    break;
                 SASSERT(idx > 0);
                 --idx;
             }