From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 22 Jul 2013 23:11:59 +0000 (-0400)
Subject: Allow BV and DT in either order in the logic string
X-Git-Tag: cvc5-1.0.0~7287^2~51
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36b4c5c156e32d7bb8634794e8bf95b8617a3944;p=cvc5.git

Allow BV and DT in either order in the logic string
---

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index cbd0b510e..008618342 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -181,6 +181,7 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_UF);
         p += 2;
       }
+      // allow BV or DT in either order
       if(!strncmp(p, "BV", 2)) {
         enableTheory(THEORY_BV);
         p += 2;
@@ -189,6 +190,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_DATATYPES);
         p += 2;
       }
+      if(!d_theories[THEORY_BV] && !strncmp(p, "BV", 2)) {
+        enableTheory(THEORY_BV);
+        p += 2;
+      }
       if(!strncmp(p, "IDL", 3)) {
         enableIntegers();
         disableReals();