diff options
| -rw-r--r-- | src/smt/set_defaults.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c887d1895..8236486dd 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -300,7 +300,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } // Disable options incompatible with incremental solving, unsat cores, and - // proofs or output an error if enabled explicitly + // proofs or output an error if enabled explicitly. It is also currently + // incompatible with arithmetic, force the option off. if (options::incrementalSolving() || options::unsatCores() || options::proof()) { @@ -326,8 +327,9 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) bool uncSimp = !logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() - && (logic.isTheoryEnabled(THEORY_ARRAYS) - && logic.isTheoryEnabled(THEORY_BV)); + && logic.isTheoryEnabled(THEORY_ARRAYS) + && logic.isTheoryEnabled(THEORY_BV) + && !logic.isTheoryEnabled(THEORY_ARITH); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; options::unconstrainedSimp.set(uncSimp); |