summaryrefslogtreecommitdiff
path: root/src/theory/arrays/array_proof_reconstruction.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-10-25 14:28:07 -0700
committerAina Niemetz <aina.niemetz@gmail.com>2017-10-25 14:28:07 -0700
commit0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (patch)
treed0a60841c95046ab9b19923d393f663805e962da /src/theory/arrays/array_proof_reconstruction.h
parentc49ef48588c708bfef3c7a0f9db8219415301a94 (diff)
Switching EqProof to use shared_ptr everywhere. (#1217)
This clarifies the memory ownership of EqProofs.
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.h')
-rw-r--r--src/theory/arrays/array_proof_reconstruction.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index c5ba21569..1b06dc524 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -34,7 +34,8 @@ public:
ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
void notify(unsigned reasonType, Node reason, Node a, Node b,
- std::vector<TNode>& equalities, eq::EqProof* proof) const;
+ std::vector<TNode>& equalities,
+ eq::EqProof* proof) const override;
void setRowMergeTag(unsigned tag);
void setRow1MergeTag(unsigned tag);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback