From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 8 Jan 2014 16:17:32 +0000 (-0500)
Subject: Fix LogicInfo parsing for string logics
X-Git-Tag: cvc5-1.0.0~7163
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d79c1a1903ee90e91500c1c87b262c3a38b5765;p=cvc5.git

Fix LogicInfo parsing for string logics
---

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index d74f36069..525b129cf 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -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();