diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-08 10:33:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-08 10:33:59 -0700 |
| commit | 7b36dc4ee0f4fa5c1d73b0f648c74b9736a5f626 (patch) | |
| tree | e8b7631755e92c80536e9a146bbd6c5e53a99787 /test | |
| parent | be3543ef7e01eb32aab3161fa2778953fabc988d (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.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/div_mod.cvc | 10 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5c31c4fe1..b92f767b2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -289,6 +289,7 @@ set(regress_0_tests regress0/bv/core/slice-18.smtv1.smt2 regress0/bv/core/slice-19.smtv1.smt2 regress0/bv/core/slice-20.smtv1.smt2 + regress0/bv/div_mod.cvc regress0/bv/divtest_2_5.smt2 regress0/bv/divtest_2_6.smt2 regress0/bv/eager-inc-cadical.smt2 diff --git a/test/regress/regress0/bv/div_mod.cvc b/test/regress/regress0/bv/div_mod.cvc new file mode 100644 index 000000000..3f31bdd70 --- /dev/null +++ b/test/regress/regress0/bv/div_mod.cvc @@ -0,0 +1,10 @@ +% EXPECT: entailed + +x : BITVECTOR(4); + +QUERY +( BVUDIV(x, 0bin0000) = 0bin1111 ) AND +( BVUREM(x, 0bin0000) = x ) AND +( BVSDIV(x, 0bin0000) = 0bin1111 OR BVSDIV(x, 0bin0000) = 0bin0001 ) AND +( BVSREM(x, 0bin0000) = x ) AND +( BVSMOD(x, 0bin0000) = x ); |