From: yoni206 <yoni206@users.noreply.github.com>
Date: Sat, 14 Apr 2018 05:58:37 +0000 (-0700)
Subject: allowing --bool-to-bv without quantifiers (#1771)
X-Git-Tag: cvc5-1.0.0~5153
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25e77125743b97b9f36d2344a3b5598ab64223b9;p=cvc5.git

allowing --bool-to-bv without quantifiers (#1771)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ea51df8c9..57cf3ac8c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1472,9 +1472,11 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if (options::cbqiBv()) {
+  if (options::cbqiBv() && d_logic.isQuantified())
+  {
     if(options::boolToBitvector.wasSetByUser()) {
-      throw OptionException("bool-to-bv not supported with CBQI BV");
+      throw OptionException(
+          "bool-to-bv not supported with CBQI BV for quantified logics");
     }
     Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
              << endl;
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index f9f66a0be..b0f7a2cb8 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -2834,7 +2834,8 @@ Node BvInverter::solveBvLit(Node sv,
   litk = k = lit.getKind();
 
   /* Note: option --bool-to-bv is currently disabled when CBQI BV
-   *       is enabled. We currently do not support Boolean operators
+   *       is enabled and the logic is quantified. 
+   *       We currently do not support Boolean operators
    *       that are interpreted as bit-vector operators of width 1.  */
 
   /* Boolean layer ----------------------------------------------- */