diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-08 11:18:02 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-08 11:18:02 -0500 |
commit | 7d8edf70f60c31d0f7d63a99eea682f96382aecf (patch) | |
tree | aa458b35acf6ad71789bb89ee012d4db83186647 /src/theory/logic_info.cpp | |
parent | 1e1ba9ff90b760ff7a029b479c659baca16b5a1e (diff) |
Fix LogicInfo parsing for string logics
Diffstat (limited to 'src/theory/logic_info.cpp')
-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(); |