From 2d08baf3d577ad972450cbe92d3457156265f2f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 May 2020 12:20:40 -0700 Subject: [PATCH] fix #4219 --- src/smt/theory_pb.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index d78556f3d..11c83a9d4 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -2044,7 +2044,7 @@ namespace smt { } bool theory_pb::is_proof_justification(justification const& j) const { - return typeid(smt::justification_proof_wrapper) == typeid(j); + return typeid(smt::justification_proof_wrapper) == typeid(j) || get_manager().proofs_enabled(); } justification* theory_pb::justify(literal l1, literal l2) {