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

author	Guy <katz911@gmail.com>
	Thu, 2 Jun 2016 00:41:17 +0000 (17:41 -0700)
committer	Guy <katz911@gmail.com>
	Thu, 2 Jun 2016 00:41:17 +0000 (17:41 -0700)
commit	de0dd1dc966b05467f1a5443ff33094262f5076a
tree	46a8539229fc31226b416755e6a88c18476ecffc	tree
parent	89ba584531115b7f6d47088d7614368ea05ab9d8	commit \| diff

Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

50 files changed:

proofs/signatures/th_arrays.plf		diff \| blob \| history
proofs/signatures/th_bv.plf		diff \| blob \| history
proofs/signatures/th_bv_bitblast.plf		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/options/Makefile.am		diff \| blob \| history
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/bitvector_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.h		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/lemma_proof.cpp	[deleted file]	blob \| history
src/proof/lemma_proof.h	[deleted file]	blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/proof_output_channel.cpp	[deleted file]	blob \| history
src/proof/proof_output_channel.h	[deleted file]	blob \| history
src/proof/proof_utils.cpp		diff \| blob \| history
src/proof/proof_utils.h		diff \| blob \| history
src/proof/sat_proof_implementation.h		diff \| blob \| history
src/proof/skolemization_manager.h		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/theory_proof.h		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/proof/uf_proof.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine_check_proof.cpp		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/abstraction.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.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
test/regress/regress0/aufbv/Makefile.am		diff \| blob \| history

RSS Atom