From 7f396917c481de7a57782a5daf31992c37d7d964 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 2 Oct 2020 17:25:29 +0200 Subject: [PATCH] Allow for theory combination of strings with nonlinear real arithmetic. (#5111) This PR makes sure that enabling strings and nonlinear real arithmetic at the same time works fine. Right now, the configuration for strings enforces linear arithmetic if no integers are enabled, in particular for NRA. Fixed #5109. --- src/smt/set_defaults.cpp | 9 +++++++-- 1 file 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(); } -- 2.30.2