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 /NEWS | |
| 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 'NEWS')
| -rw-r--r-- | NEWS | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -22,9 +22,15 @@ Changes: BSD-licensed Editline. Compiling with `--best` now enables Editline, instead of Readline. Without selecting optional GPL components, Editline-enabled CVC4 builds will be BSD licensed. +* The semantics for division and remainder operators in the CVC language now + correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero + modulus results in a constant value, instead of an uninterpreted one). + Similarly, when no language is set, the API semantics now correspond to the + SMT-LIB 2.6 semantics. * The `competition` build type includes the dependencies used for SMT-COMP by default. Note that this makes this build type produce GPL-licensed binaries. + Changes since 1.7 ================= |