diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 02:48:22 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-17 00:48:22 -0700 |
| commit | 29ae7d5ec0a73b90529e2200d948e6f4051099f1 (patch) | |
| tree | a9dcb7074a2e79b35e17f2c4483638cf91ea1093 /src/smt/smt_engine.cpp | |
| parent | 4d303b5e6de8a3b963357a3c0238ffe81d36f766 (diff) | |
Eliminate partial operators in sygus grammar normalization (#2323)
This corrects a bug that was introduced in #2266 (the hack removed there was necessary).
This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.
This also enables total semantics for BV div-by-zero for sygus.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 34a5a6d5b..418028d09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1216,8 +1216,12 @@ void SmtEngine::setDefaults() { // Language-based defaults if (!options::bitvectorDivByZeroConst.wasSetByUser()) { + // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we + // 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::isInputLang_smt2_6(options::inputLanguage()) + || options::inputLanguage() == language::input::LANG_SYGUS); } bool is_sygus = false; if (options::inputLanguage() == language::input::LANG_SYGUS) |