From 3b50dfe623f44e97d85449fa2a7566e81c639b47 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 May 2020 11:47:47 -0500 Subject: [PATCH] Do not enable unconstrained simplification if arithmetic is present (#4489) For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71). --- src/smt/set_defaults.cpp | 8 +++++--- 1 file 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); -- 2.30.2