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) {