From 0059e880365518bd2d9938927b17079aa47a8c9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Feb 2022 20:10:32 +0200 Subject: [PATCH] fix #5808 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index ef0fdfedd..0dc52c1b2 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1881,11 +1881,13 @@ 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 << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";); - return false; - } unsigned num_lits = cls.get_num_literals(); + if (cjs && typeid(smt::unit_resolution_justification) == typeid(*cjs)) + ; + else if (cjs && !is_proof_justification(*cjs)) { + TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";); + break; + } if (cls.get_literal(0) == conseq) { process_antecedent(cls.get_literal(1), offset); }