From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 27 May 2016 21:28:24 +0000 (-0700)
Subject: Enabled bit-blasting option for QF_UFBV
X-Git-Tag: cvc5-1.0.0~6049^2~26
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d058f9aacac64bbe384995e81af92cb8b2bb032d;p=cvc5.git

Enabled bit-blasting option for QF_UFBV
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e4b9023d5..8f282b413 100644
--- 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.");