From: Liana Hadarean <lianahady@gmail.com>
Date: Thu, 15 Nov 2012 20:52:09 +0000 (+0000)
Subject: changed logic options so that justification is turned on for QF_ABV and QF_UFBV as... 
X-Git-Tag: cvc5-1.0.0~7590
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=263ec763ab08a137b7997c7b2c536a22aa6496f6;p=cvc5.git

changed logic options so that justification is turned on for QF_ABV and QF_UFBV as well
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16de7957a..69aec695c 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);
@@ -848,10 +848,10 @@ void SmtEngine::setLogicInternal() throw() {
         (not d_logic.isQuantified() &&
           d_logic.isPure(THEORY_BV)
           ) ||
-        // QF_AUFBV
+        // QF_AUFBV or QF_ABV or QF_UFBV
         (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-         d_logic.isTheoryEnabled(THEORY_UF) &&
+         (d_logic.isTheoryEnabled(THEORY_ARRAY) ||
+          d_logic.isTheoryEnabled(THEORY_UF)) &&
          d_logic.isTheoryEnabled(THEORY_BV)
          ) ||
         // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)