diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 20800b0b3..7be53ff86 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1779,7 +1779,7 @@ namespace smt { justification* theory_pb::justify(literal_vector const& lits) { justification* js = 0; if (proofs_enabled()) { - js = get_context().mk_justification(theory_axiom_justification(get_id(), get_context(), lits.size(), lits.c_ptr())); + js = get_context().mk_justification(theory_axiom_justification(get_id(), get_context().get_region(), lits.size(), lits.c_ptr())); } return js; }