From a7aba0c8580d5153fee99b4d59345e33c39c893b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 22 Oct 2020 20:06:51 +0200 Subject: [PATCH] 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. --- src/smt/set_defaults.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4402beba2..27959a6bc 100644 --- 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); -- 2.30.2