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 /src/smt | |
| 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 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 236137bb2..aa0e976f2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -89,8 +89,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // set this option if the input format is SMT LIB 2.6. We also set this // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus. options::bitvectorDivByZeroConst.set( - language::isInputLang_smt2_6(options::inputLanguage()) - || language::isInputLangSygus(options::inputLanguage())); + !language::isInputLang_smt2_5(options::inputLanguage(), true)); } bool is_sygus = language::isInputLangSygus(options::inputLanguage()); |