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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 22 Feb 2021 22:07:16 +0000 (16:07 -0600)
committer	GitHub <noreply@github.com>
	Mon, 22 Feb 2021 22:07:16 +0000 (16:07 -0600)
commit	71d72df0437607723256bbd7b4f28cd6c89fe40f
tree	1021b9e166290db4637a0be447da359d0aed4752	tree
parent	580f3e93c2cc4564e6fa87d07426dc1ff87224e4	commit \| diff

(proof-new) Change proof-new option to proof (#5955)

Also moves several proof-specific options to proof_options.

26 files changed:

src/expr/lazy_proof_chain.cpp		diff \| blob \| history
src/expr/proof_checker.cpp		diff \| blob \| history
src/expr/proof_ensure_closed.cpp		diff \| blob \| history
src/expr/proof_ensure_closed.h		diff \| blob \| history
src/expr/proof_node_algorithm.cpp		diff \| blob \| history
src/expr/proof_node_manager.cpp		diff \| blob \| history
src/expr/proof_node_to_sexpr.cpp		diff \| blob \| history
src/expr/proof_node_updater.cpp		diff \| blob \| history
src/options/proof_options.toml		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		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/sat_proof_manager.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/proof_macros.h		diff \| blob \| history
test/regress/regress0/arith/non-normal.smt2		diff \| blob \| history