Fix issue with free variables introduced by quantifier rewriter (#5602)

This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.

This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.

1 files changed, 0 insertions, 13 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7e6bed464..ca5a2773b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -239,14 +239,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       options::fmfBound.set(true);
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
-    // Do not eliminate extended arithmetic symbols from quantified formulas,
-    // since some strategies, e.g. --re-elim-agg, introduce them.
-    if (!options::elimExtArithQuant.wasSetByUser())
-    {
-      options::elimExtArithQuant.set(false);
-      Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
-                   << std::endl;
-    }
     // Note we allow E-matching by default to support combinations of sequences
     // and quantifiers.
   }
@@ -935,11 +927,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
     }
-    // do not eliminate extended arithmetic symbols from quantified formulas
-    if (!options::elimExtArithQuant.wasSetByUser())
-    {
-      options::elimExtArithQuant.set(false);
-    }
     if (!options::eMatching.wasSetByUser())
     {
       options::eMatching.set(options::fmfInstEngine());