Fix LogicInfo parsing for string logics
authorMorgan Deters <mdeters@cs.nyu.edu>
Wed, 8 Jan 2014 16:17:32 +0000 (11:17 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Wed, 8 Jan 2014 16:17:32 +0000 (11:17 -0500)
src/theory/logic_info.cpp

index d74f3606932ada2572d984400e3cc47fdade6daf..525b129cf969fc949ec4fa555155ffdb4b231303 100644 (file)
@@ -181,16 +181,6 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_ARRAY);
         ++p;
       }
-      if(*p == 'S') {
-        // Strings requires arith for length constraints,
-        // and UF for equality (?)
-        enableTheory(THEORY_STRINGS);
-        enableTheory(THEORY_UF);
-        enableTheory(THEORY_ARITH);
-        enableIntegers();
-        arithOnlyLinear();
-        ++p;
-      }
       if(!strncmp(p, "UF", 2)) {
         enableTheory(THEORY_UF);
         p += 2;
@@ -208,6 +198,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_BV);
         p += 2;
       }
+      if(*p == 'S') {
+        // Strings requires arith for length constraints,
+        // and UF for equality (?)
+        enableTheory(THEORY_STRINGS);
+        enableTheory(THEORY_UF);
+        enableTheory(THEORY_ARITH);
+        enableIntegers();
+        arithOnlyLinear();
+        ++p;
+      }
       if(!strncmp(p, "IDL", 3)) {
         enableIntegers();
         disableReals();