diff options
| -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() ){ |