forgot to uncomment setLogicInternal for THEORY_BV

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 69aec695c5a484cb4a432dfad1bd1b6f5a936c35..425892583430162aab646dc5ba7fa978212655d8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -720,8 +720,8 @@ void SmtEngine::setLogicInternal() throw() {
   d_logic.lock();
 
   // may need to force uninterpreted functions to be on for non-linear
-  if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) /*||
-      d_logic.isTheoryEnabled(theory::THEORY_BV)*/) &&
+  if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) ||
+      d_logic.isTheoryEnabled(theory::THEORY_BV)) &&
      !d_logic.isTheoryEnabled(theory::THEORY_UF)){
     d_logic = d_logic.getUnlockedCopy();
     d_logic.enableTheory(theory::THEORY_UF);