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

author	Liana Hadarean <lianahady@gmail.com>
	Thu, 23 Apr 2015 16:38:48 +0000 (17:38 +0100)
committer	Liana Hadarean <lianahady@gmail.com>
	Thu, 23 Apr 2015 16:38:48 +0000 (17:38 +0100)
commit	0daf670d46ec2e781c2060b41449f2787b6e8f66
tree	7f1870bc621407a3c387ab6eb3dc77db529355dc	tree
parent	c604492260d0555bdb3cac5ba0863b7223f21777	commit \| diff

Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

14 files changed:

src/parser/smt2/smt2.cpp		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_engine_check_proof.cpp		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/util/unsat_core.h		diff \| blob \| history
test/regress/regress0/arith/bug569.smt2		diff \| blob \| history
test/regress/regress0/datatypes/empty_tuprec.cvc		diff \| blob \| history
test/regress/regress0/fmf/Makefile	[new file with mode: 0644]	blob
test/regress/regress0/fmf/PUZ001+1.smt2		diff \| blob \| history
test/regress/run_regression		diff \| blob \| history