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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ea51df8c94a8f2772d4907c9db5735b8080146b5..57cf3ac8c72786465b9132475df02b06abcbb611 100644 (file)
--- 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 f9f66a0befbabd84a8dc02d7e0e26b2c4eabbf67..b0f7a2cb87081f1f8d4c049907a6994fcfda78c2 100644 (file)
--- 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 ----------------------------------------------- */