Add option for using bound inference for relevant assertions (#7152)

The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 034ca30e2..3c35c2961 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -649,6 +649,12 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       opts.arith.nlExtTangentPlanesInterleave = true;
     }
   }
+  if (!opts.arith.nlRlvAssertBoundsWasSetByUser)
+  {
+    // use bound inference to determine when bounds are irrelevant only when
+    // the logic is quantifier-free
+    opts.arith.nlRlvAssertBounds = !logic.isQuantified();
+  }
 
   // set the default decision mode
   setDefaultDecisionMode(logic, opts);