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);
                 }