From: Liana Hadarean <lianahady@gmail.com>
Date: Thu, 15 Nov 2012 20:57:22 +0000 (+0000)
Subject: forgot to uncomment setLogicInternal for THEORY_BV
X-Git-Tag: cvc5-1.0.0~7589
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88ef1f0be6bd712cf1ce8401416d634f61f381b4;p=cvc5.git

forgot to uncomment setLogicInternal for THEORY_BV
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 69aec695c..425892583 100644
--- 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);