Enabled bit-blasting option for QF_UFBV

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e4b9023d5a6453f05124aa611d2ab0c3c9aa0801..8f282b41391f18736f8cb57c25fb88512e64053c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1316,9 +1316,9 @@ void SmtEngine::setDefaults() {
   }
   else if (options::solveIntAsBV() > 0) {
     d_logic = LogicInfo("QF_BV");
-  // } else if (d_logic.getLogicString() == "QF_UFBV" &&
-  //            options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-  //   d_logic = LogicInfo("QF_BV");
+  } else if (d_logic.getLogicString() == "QF_UFBV" &&
+             options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+    d_logic = LogicInfo("QF_BV");
   }
 
   // set strings-exp
@@ -3877,8 +3877,8 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
-      !d_smt.d_logic.isPure(THEORY_BV)) {
-    //    && d_smt.d_logic.getLogicString() != "QF_UFBV")
+      !d_smt.d_logic.isPure(THEORY_BV) &&
+      d_smt.d_logic.getLogicString() != "QF_UFBV") {
     throw ModalException("Eager bit-blasting does not currently support theory combination. "
                          "Note that in a QF_BV problem UF symbols can be introduced for division. "
                          "Try --bv-div-zero-const to interpret division by zero as a constant.");