diff options
| -rw-r--r-- | src/smt/set_defaults.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 79490045b..468e246c4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -546,8 +546,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) LogicInfo log(logic.getUnlockedCopy()); // Strings requires arith for length constraints, and also UF needsUf = true; - if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic() - || !logic.areIntegersUsed()) + if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) { Notice() << "Enabling linear integer arithmetic because strings are enabled" @@ -556,6 +555,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) log.enableIntegers(); log.arithOnlyLinear(); } + else if (!logic.areIntegersUsed()) + { + Notice() << "Enabling integer arithmetic because strings are enabled" + << std::endl; + log.enableIntegers(); + } logic = log; logic.lock(); } |