summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-15 02:58:30 -0800
committerAndres Noetzli <andres.noetzli@gmail.com>2017-11-15 02:58:30 -0800
commit3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch)
tree6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/theory/uf
parent85df7998e4362e0a9c796146d07d7b9e91045a31 (diff)
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/theory_uf.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 170621603..f97a4b639 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -634,8 +634,8 @@ void TheoryUF::conflict(TNode a, TNode b) {
std::shared_ptr<eq::EqProof> pf =
d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
d_conflictNode = explain(a.eqNode(b), pf.get());
- ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
- d_out->conflict(d_conflictNode, puf);
+ std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr);
+ d_out->conflict(d_conflictNode, std::move(puf));
d_conflict = true;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback