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 cbd0b510e30eb81070206f333f84fdde856f2d68..0086183429c4e6013c1251867b38b65d764e47f7 100644 (file)
--- 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();