Use theoryof-mode=type for QF_NRA (#5326)

We've observed that our QF_NRA solving benefits significantly from --theoryof-mode=type across the board (of other options that influence QF_NRA solving). This PR sets type as the new default for QF_NRA solving.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4402beba26bddc26eba2c45b33bf32f6f56fc941..27959a6bcf1a4555b8bbfea5c70faf7426f3d2ec 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -604,7 +604,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
         && !logic.isTheoryEnabled(THEORY_STRINGS)
         && !logic.isTheoryEnabled(THEORY_SETS)
-        && !logic.isTheoryEnabled(THEORY_BAGS))
+        && !logic.isTheoryEnabled(THEORY_BAGS)
+        && !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+             && !logic.isQuantified()))
     {
       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
       options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);