git.libre-soc.org Git - cvc5.git/commit

author	Tim King <taking@cs.nyu.edu>
	Wed, 25 Oct 2017 21:28:07 +0000 (14:28 -0700)
committer	Aina Niemetz <aina.niemetz@gmail.com>
	Wed, 25 Oct 2017 21:28:07 +0000 (14:28 -0700)
commit	0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0
tree	d0a60841c95046ab9b19923d393f663805e962da	tree
parent	c49ef48588c708bfef3c7a0f9db8219415301a94	commit \| diff

Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

13 files changed:

src/proof/arith_proof.cpp		diff \| blob \| history
src/proof/arith_proof.h		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/array_proof.h		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/proof/uf_proof.h		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.cpp		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history