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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 15 Dec 2020 20:04:27 +0000 (14:04 -0600)
committer	GitHub <noreply@github.com>
	Tue, 15 Dec 2020 20:04:27 +0000 (14:04 -0600)
commit	002955063ecf1b4b190717a7a0b2aec79ac7b6d9
tree	9a26231f484a76f8373541c67e3c1e7156b12a6a	tree
parent	aa1b0e19f9ccfc5338a1d056f03b36c0bec6b4b4	commit \| diff

Remove bv divide by zero option (#5672)

This is required to avoid failures in the planned refactoring of check-models.

This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.

It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.

FYI @barrettcw

12 files changed:

src/options/bv_options.toml		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
test/regress/regress0/bv/divtest_2_5.smt2		diff \| blob \| history
test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2		diff \| blob \| history
test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2		diff \| blob \| history
test/regress/regress1/ho/issue4065-no-rep.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2		diff \| blob \| history

RSS Atom