From 9958cab5cc737edf443340e5e08c094d91fc0c93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Feb 2022 07:43:30 +0200 Subject: [PATCH] fix #5808 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 8cef18ab2..ef0fdfedd 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1881,10 +1881,9 @@ namespace smt { inc_coeff(conseq, offset); clause& cls = *js.get_clause(); justification* cjs = cls.get_justification(); - if (cjs && !is_proof_justification(*cjs)) { - TRACE("pb", tout << "skipping justification for clause over: " << conseq << " " - << typeid(*cjs).name() << "\n";); - break; + if (cjs && !is_proof_justification(*cjs)) { + TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";); + return false; } unsigned num_lits = cls.get_num_literals(); if (cls.get_literal(0) == conseq) {