diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-19 03:37:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-19 01:37:26 -0700 |
| commit | 94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613 (patch) | |
| tree | fb02a35e8ab26468f02e373ccab13bd710dfd6d5 /src/smt/smt_engine.cpp | |
| parent | d862942f821ea14973207ef538be3326fb11c17c (diff) | |
SyGuS must use total bitvector division (#4119)
Our SyGuS utilities are not designed to deal with partial bitvector division. If a user forced an older version of SMT-LIB semantics while using SyGuS, this led to a number of issues.
For now, we disable this option when it is combined with SyGuS, regardless of whether the user turns it on.
A more permanent solution will be to remove the old SMT-LIB semantics option bv-div-zero-const entirely.
Fixes #4097 and fixes #4088 and fixes #4104.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4b2326696..1d096e1fe 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2004,7 +2004,16 @@ void SmtEngine::setDefaults() { } } //do not allow partial functions - if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ + if (!options::bitvectorDivByZeroConst()) + { + if (options::bitvectorDivByZeroConst.wasSetByUser()) + { + throw OptionException( + "--no-bv-div-zero-const is not supported with SyGuS"); + } + Notice() + << "SmtEngine: setting bv-div-zero-const to true to support SyGuS" + << std::endl; options::bitvectorDivByZeroConst.set( true ); } if( !options::dtRewriteErrorSel.wasSetByUser() ){ |