From 36b4c5c156e32d7bb8634794e8bf95b8617a3944 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 22 Jul 2013 19:11:59 -0400
Subject: [PATCH] Allow BV and DT in either order in the logic string

---
 src/theory/logic_info.cpp | 5 +++++
 1 file changed, 5 insertions(+)

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();
-- 
2.30.2