diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-08 11:17:32 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-08 11:17:32 -0500 |
commit | 4d79c1a1903ee90e91500c1c87b262c3a38b5765 (patch) | |
tree | f8668cab85cf794d747b413e4f94eab2f42f2ce3 /src | |
parent | c21473e09b7376f28d2d49cc78a878582432fed8 (diff) |
Fix LogicInfo parsing for string logics
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/logic_info.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
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(); |