From f47cc702362d8d64ab5462ade705a4426ed21a85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2015 11:48:52 -0700 Subject: [PATCH] use of regions for AUX lemmas from pb solver Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 1eff86db4..20800b0b3 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1771,7 +1771,7 @@ namespace smt { literal lits[2] = { l1, l2 }; justification* js = 0; if (proofs_enabled()) { - js = alloc(theory_axiom_justification, get_id(), get_context().get_region(), 2, lits); + js = get_context().mk_justification(theory_axiom_justification(get_id(), get_context().get_region(), 2, lits)); } return js; } @@ -1779,7 +1779,7 @@ namespace smt { justification* theory_pb::justify(literal_vector const& lits) { justification* js = 0; if (proofs_enabled()) { - js = alloc(theory_lemma_justification, get_id(), get_context(), lits.size(), lits.c_ptr()); + js = get_context().mk_justification(theory_axiom_justification(get_id(), get_context(), lits.size(), lits.c_ptr())); } return js; }