From 4145b92136294e07604048a3d588de6d9bc3e77c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2015 11:52:07 -0700 Subject: [PATCH] use of regions for AUX lemmas from pb solver Signed-off-by: Nikolaj Bjorner --- 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 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; }