From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Mar 2020 08:37:26 +0000 (-0500)
Subject: SyGuS must use total bitvector division (#4119)
X-Git-Tag: cvc5-1.0.0~3474
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613;p=cvc5.git

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.
---

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