diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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); |