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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 79490045b3a73cc571b4c2c0e8d2a0c55a999391..468e246c4814228379c3fbd27a47fcd1644ac6b2 100644 (file)
--- 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();
   }