From 94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Mar 2020 03:37:26 -0500 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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() ){ -- 2.30.2