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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Thu, 15 Jul 2021 01:27:33 +0000 (18:27 -0700)
committer	GitHub <noreply@github.com>
	Thu, 15 Jul 2021 01:27:33 +0000 (18:27 -0700)
commit	ffdf7434ba53191546e13663764894852e8bc6dd
tree	8e312810250f7feb27b8845fce710996b979069d	tree
parent	e3cd14dcc00eddef1238dce4e9c90be18858bb73	commit \| diff

bv: Rename simple solver to bitblast-internal. (#6888)

18 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/bv_options.toml		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_bitblast_internal.h	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_simple.cpp	[deleted file]	blob \| history
src/theory/bv/bv_solver_simple.h	[deleted file]	blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
test/regress/regress0/bv/ackermann1.smt2		diff \| blob \| history
test/regress/regress0/bv/bool-model.smt2		diff \| blob \| history
test/regress/regress0/bv/bool-to-bv-ite.smt2		diff \| blob \| history
test/regress/regress0/bv/bug734.smt2		diff \| blob \| history
test/regress/regress0/bv/issue-4076.smt2		diff \| blob \| history
test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2		diff \| blob \| history
test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2		diff \| blob \| history
test/regress/regress0/proofs/open-pf-rederivation.smt2		diff \| blob \| history
test/regress/regress1/bug520.smt2		diff \| blob \| history