diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-15 02:58:30 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-15 02:58:30 -0800 |
commit | 3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch) | |
tree | 6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/theory/arrays | |
parent | 85df7998e4362e0a9c796146d07d7b9e91045a31 (diff) |
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b43ba5591..af417f740 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2245,15 +2245,17 @@ void TheoryArrays::conflict(TNode a, TNode b) { d_conflictNode = explain(a.eqNode(b), proof.get()); if (!d_inCheckModel) { - ProofArray* proof_array = NULL; + std::unique_ptr<ProofArray> proof_array; if (d_proofsEnabled) { proof->debug_print("pf::array"); - proof_array = new ProofArray(proof, /*row=*/d_reasonRow, - /*row1=*/d_reasonRow1, /*ext=*/d_reasonExt); + proof_array.reset(new ProofArray(proof, + /*row=*/d_reasonRow, + /*row1=*/d_reasonRow1, + /*ext=*/d_reasonExt)); } - d_out->conflict(d_conflictNode, proof_array); + d_out->conflict(d_conflictNode, std::move(proof_array)); } d_conflict = true; |