projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be3543e) | patch
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 8 Sep 2020 17:33:59 +0000 (10:33 -0700)
committerGitHub <noreply@github.com>
Tue, 8 Sep 2020 17:33:59 +0000 (10:33 -0700)
commit7b36dc4ee0f4fa5c1d73b0f648c74b9736a5f626
treee8b7631755e92c80536e9a146bbd6c5e53a99787tree
parentbe3543ef7e01eb32aab3161fa2778953fabc988dcommit | diff
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)

This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.
NEWS diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/options/bv_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/div_mod.cvc [new file with mode: 0644] blob