Do not expand theory definitions at the beginning of preprocessing (#5544)

This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.

This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.

This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.

The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).

49 files changed, 160 insertions, 42 deletions

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index fe3dbc62b..c2374c6ff 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -130,7 +130,11 @@ bool ProcessAssertions::apply(Assertions& as)
       << "ProcessAssertions::processAssertions() : pre-definition-expansion"
       << endl;
   dumpAssertions("pre-definition-expansion", assertions);
-  d_exDefs.expandAssertions(assertions, false);
+  // Expand definitions, which replaces defined functions with their definition
+  // and does beta reduction. Notice we pass true as the second argument since
+  // we do not want to call theories to expand definitions here, since we want
+  // to give the opportunity to rewrite/preprocess terms before expansion.
+  d_exDefs.expandAssertions(assertions, true);
   Trace("smt-proc")
       << "ProcessAssertions::processAssertions() : post-definition-expansion"
       << endl;
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 577407c07..142f02eab 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -25,7 +25,10 @@ ArithPreprocess::ArithPreprocess(ArithState& state,
     : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
 {
 }
-TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); }
+TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly)
+{
+  return d_opElim.eliminate(n, partialOnly);
+}
 bool ArithPreprocess::reduceAssertion(TNode atom)
 {
   context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 165209bd9..622357e73 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -46,8 +46,13 @@ class ArithPreprocess
    * Call eliminate operators on formula n, return the resulting trust node,
    * which is of TrustNodeKind REWRITE and whose node is the result of
    * eliminating extended operators from n.
+   *
+   * @param n The node to eliminate operators from
+   * @param partialOnly Whether we are eliminating partial operators only.
+   * @return the trust node proving (= n nr) where nr is the return of
+   * eliminating operators in n, or the null trust node if n was unchanged.
    */
-  TrustNode eliminate(TNode n);
+  TrustNode eliminate(TNode n, bool partialOnly = false);
   /**
    * Reduce assertion. This sends a lemma via the inference manager if atom
    * contains any extended operators. When applicable, the lemma is of the form:
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 4d4c4a6f5..fbd1798cd 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -46,21 +46,23 @@ void OperatorElim::checkNonLinearLogic(Node term)
   }
 }
 
-TrustNode OperatorElim::eliminate(Node n)
+TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
 {
   TConvProofGenerator* tg = nullptr;
-  Node nn = eliminateOperators(n, tg);
+  Node nn = eliminateOperators(n, tg, partialOnly);
   if (nn != n)
   {
     // since elimination may introduce new operators to eliminate, we must
     // recursively eliminate result
-    Node nnr = eliminateOperatorsRec(nn, tg);
+    Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
     return TrustNode::mkTrustRewrite(n, nnr, nullptr);
   }
   return TrustNode::null();
 }
 
-Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperatorsRec(Node n,
+                                         TConvProofGenerator* tg,
+                                         bool partialOnly)
 {
   Trace("arith-elim") << "Begin elim: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
@@ -108,12 +110,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
-      Node retElim = eliminateOperators(ret, tg);
+      Node retElim = eliminateOperators(ret, tg, partialOnly);
       if (retElim != ret)
       {
         // recursively eliminate operators in result, since some eliminations
         // are defined in terms of other non-standard operators.
-        ret = eliminateOperatorsRec(retElim, tg);
+        ret = eliminateOperatorsRec(retElim, tg, partialOnly);
       }
       visited[cur] = ret;
     }
@@ -123,7 +125,9 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
   return visited[n];
 }
 
-Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperators(Node node,
+                                      TConvProofGenerator* tg,
+                                      bool partialOnly)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
@@ -143,6 +147,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     case TO_INTEGER:
     case IS_INTEGER:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node toIntSkolem;
       std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
       if (it == d_to_int_skolem.end())
@@ -180,6 +189,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     case INTS_DIVISION_TOTAL:
     case INTS_MODULUS_TOTAL:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node den = Rewriter::rewrite(node[1]);
       Node num = Rewriter::rewrite(node[0]);
       Node intVar;
@@ -283,6 +297,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     }
     case DIVISION_TOTAL:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node num = Rewriter::rewrite(node[0]);
       Node den = Rewriter::rewrite(node[1]);
       if (den.isConst())
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index c7b55caf1..bca80ea4d 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -37,7 +37,7 @@ class OperatorElim : public EagerProofGenerator
     * transcendental functions), then we replace it by a form that eliminates
     * that operator. This may involve the introduction of witness terms.
     */
-  TrustNode eliminate(Node n);
+  TrustNode eliminate(Node n, bool partialOnly = false);
   /**
    * Get axiom for term n. This returns the axiom that this class uses to
    * eliminate the term n, which is determined by its top-most symbol.
@@ -101,7 +101,7 @@ class OperatorElim : public EagerProofGenerator
    * @param n The node to eliminate operators from.
    * @return The (single step) eliminated form of n.
    */
-  Node eliminateOperators(Node n, TConvProofGenerator* tg);
+  Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
   /**
    * Recursively ensure that n has no non-standard operators. This applies
    * the above method on all subterms of n.
@@ -109,7 +109,7 @@ class OperatorElim : public EagerProofGenerator
    * @param n The node to eliminate operators from.
    * @return The eliminated form of n.
    */
-  Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg);
+  Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly);
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 247772897..b8cead4fc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -97,6 +97,12 @@ void TheoryArith::preRegisterTerm(TNode n)
   d_internal->preRegisterTerm(n);
 }
 
+TrustNode TheoryArith::expandDefinition(Node node)
+{
+  // call eliminate operators, to eliminate partial operators only
+  return d_arithPreproc.eliminate(node, true);
+}
+
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 
 TrustNode TheoryArith::ppRewrite(TNode atom)
@@ -140,8 +146,9 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n)
   // theories may generate lemmas that involve non-standard operators. For
   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
   // introduce non-standard arithmetic terms appearing in grammars.
-  // call eliminate operators
-  return d_arithPreproc.eliminate(n);
+  // call eliminate operators. In contrast to expandDefinitions, we eliminate
+  // *all* extended arithmetic operators here, including total ones.
+  return d_arithPreproc.eliminate(n, false);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e6029faef..e26ff51ef 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -68,7 +68,11 @@ class TheoryArith : public Theory {
   /** finish initialization */
   void finishInit() override;
   //--------------------------------- end initialization
-
+  /**
+   * Expand definition, which eliminates extended operators like div/mod in
+   * the given node.
+   */
+  TrustNode expandDefinition(Node node) override;
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3e59aebe6..4d4ec89b4 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -318,6 +318,12 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
 
 TrustNode TheoryArrays::ppRewrite(TNode term)
 {
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(term);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   if (!d_preprocess)
   {
     return TrustNode::null();
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d43fa3927..7285b6768 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -200,7 +200,16 @@ Theory::PPAssertStatus TheoryBV::ppAssert(
   return d_internal->ppAssert(tin, outSubstitutions);
 }
 
-TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
+TrustNode TheoryBV::ppRewrite(TNode t)
+{
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(t);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
+  return d_internal->ppRewrite(t);
+}
 
 void TheoryBV::presolve() { d_internal->presolve(); }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 74c822215..ff36216c2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -431,6 +431,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 {
   Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+  // external selectors should be preprocessed away by now
+  Assert(n.getKind() != APPLY_SELECTOR);
   // must ensure the type is well founded and has no nested recursion if
   // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();
@@ -595,7 +597,12 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
 TrustNode TheoryDatatypes::ppRewrite(TNode in)
 {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
-
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(in);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   if( in.getKind()==EQUAL ){
     Node nn;
     std::vector< Node > rew;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 01fab92c8..ce423a7fe 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -454,6 +454,12 @@ TrustNode TheoryFp::expandDefinition(Node node)
 TrustNode TheoryFp::ppRewrite(TNode node)
 {
   Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(node);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
 
   Node res = node;
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 59666f6fd..aa847d8ea 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1612,7 +1612,10 @@ void CegInstantiator::registerCounterexampleLemma(Node lem,
       // already processed variable
       continue;
     }
-    if (ces.getType().isBoolean())
+    // must avoid selector symbols, and function skolems introduced by
+    // theory preprocessing
+    TypeNode ct = ces.getType();
+    if (ct.isBoolean() || ct.isFunctionLike())
     {
       // Boolean variables, including the counterexample literal, don't matter
       // since they are always assigned a model value.
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 57778b4c8..615ff987a 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -126,6 +126,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
   {
     return;
   }
+  Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   FirstOrderModel* m = d_quantEngine->getModel();
   std::vector<Node> lemmas;
@@ -134,6 +135,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
        ++it)
   {
     Node q = it->first;
+    Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
     if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
         && d_added_split.find(q) == d_added_split.end())
     {
@@ -196,5 +198,6 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
     d_quantEngine->addLemma(lem, false);
   }
+  Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
 }
 
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0e6ab1b18..e4f281de8 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -68,6 +68,9 @@ void TheorySets::finishInit()
   d_valuation.setUnevaluatedKind(COMPREHENSION);
   // choice is used to eliminate witness
   d_valuation.setUnevaluatedKind(WITNESS);
+  // Universe set is not evaluated. This is moreover important for ensuring that
+  // we do not eliminate terms whose value involves the universe set.
+  d_valuation.setUnevaluatedKind(UNIVERSE_SET);
 
   // functions we are doing congruence over
   d_equalityEngine->addFunctionKind(SINGLETON);
@@ -128,6 +131,11 @@ void TheorySets::preRegisterTerm(TNode node)
 
 TrustNode TheorySets::expandDefinition(Node n)
 {
+  return d_internal->expandDefinition(n);
+}
+
+TrustNode TheorySets::ppRewrite(TNode n)
+{
   Kind nk = n.getKind();
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
       || nk == COMPREHENSION)
@@ -150,7 +158,8 @@ TrustNode TheorySets::expandDefinition(Node n)
       throw LogicException(ss.str());
     }
   }
-  return d_internal->expandDefinition(n);
+  // just expand definitions
+  return expandDefinition(n);
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a5f8fa4d8..3b95c7e00 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -77,6 +77,7 @@ class TheorySets : public Theory
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
   TrustNode expandDefinition(Node n) override;
+  TrustNode ppRewrite(TNode n) override;
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
   void presolve() override;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 110ff9b2d..72a4ae50d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -997,6 +997,12 @@ void TheoryStrings::checkRegisterTermsNormalForms()
 TrustNode TheoryStrings::ppRewrite(TNode atom)
 {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(atom);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   TrustNode ret;
   Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index da0fc8de4..84212fa1b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1402,7 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   // get the node
   Node node = tlemma.getNode();
   Node lemma = tlemma.getProven();
-  Trace("te-lemma") << "Lemma, input: " << lemma << std::endl;
+  Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p
+                    << std::endl;
 
   Assert(!expr::hasFreeVar(lemma));
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 09ce71577..5298a2ca9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1689,7 +1689,6 @@ set(regress_1_tests
   regress1/quantifiers/smtlib46f14a.smt2
   regress1/quantifiers/smtlibe99bbe.smt2
   regress1/quantifiers/smtlibf957ea.smt2
-  regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   regress1/quantifiers/sygus-infer-nested.smt2
   regress1/quantifiers/symmetric_unsat_7.smt2
   regress1/quantifiers/var-eq-trigger.smt2
@@ -2159,7 +2158,6 @@ set(regress_2_tests
   regress2/bv_to_int_5095_2.smt2
   regress2/bv_to_int_ashr.smt2
   regress2/bv_to_int_bitwise.smt2
-  regress2/bv_to_int_bvmul1.smt2
   regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
@@ -2586,6 +2584,8 @@ set(regression_disabled_tests
   regress1/quantifiers/nl-pow-trick.smt2
   # timeout after changes to nonlinear on PR #5351
   regress1/quantifiers/rel-trigger-unusable.smt2
+  # changes to expand definitions, related to trigger selection for selectors
+  regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/subtype-param-unk.smt2
   regress1/quantifiers/subtype-param.smt2
@@ -2620,6 +2620,8 @@ set(regression_disabled_tests
   # timeout on debug
   regress2/arith/real2int-test.smt2
   regress2/bug396.smt2
+  # due to bv2int not handling unsigned/signed division
+  regress2/bv_to_int_bvmul1.smt2
   regress2/nl/dumortier-050317.smt2
   regress2/nl/nt-lemmas-bad.smt2
   regress2/quantifiers/ForElimination-scala-9.smt2
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 76bc4095f..c7771d5c9 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_LIA)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2
index 290850d1a..c871226ce 100644
--- a/test/regress/regress0/arith/issue3413.smt2
+++ b/test/regress/regress0/arith/issue3413.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_NIA)
 (declare-fun a () Int)
 (declare-fun e () Int)
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
index 3b84b7aff..e4bac6a0a 100644
--- a/test/regress/regress0/bug484.smt2
+++ b/test/regress/regress0/bug484.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 
 ; Preamble  --------------
diff --git a/test/regress/regress0/datatypes/issue2838.cvc b/test/regress/regress0/datatypes/issue2838.cvc
index 95e1c898a..9fab5f423 100644
--- a/test/regress/regress0/datatypes/issue2838.cvc
+++ b/test/regress/regress0/datatypes/issue2838.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 Ints_0 : ARRAY INT OF INT;
 C : TYPE = [# i : INT #];
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
index e4e1f65b4..5d0d8f6e6 100644
--- a/test/regress/regress0/fmf/fmc_unsound_model.smt2
+++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 ; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
index d951e6c50..890e765aa 100644
--- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2
index 794eefb37..0249462ee 100644
--- a/test/regress/regress1/arith/issue4985-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985-model-success.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
 (declare-const arr0 (Array Real Real))
diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2
index eae8d369d..22b55c87f 100644
--- a/test/regress/regress1/arith/issue4985b-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985b-model-success.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
 (declare-const a (Array Real Real))
diff --git a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
index f1d20befc..33c1796f9 100644
--- a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
+++ b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2
index c4a40ccc1..4bf21d533 100644
--- a/test/regress/regress1/fmf/german169.smt2
+++ b/test/regress/regress1/fmf/german169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2
index 25dc80223..6162b4cfe 100644
--- a/test/regress/regress1/fmf/issue3626.smt2
+++ b/test/regress/regress1/fmf/issue3626.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound --no-cegqi
+; COMMAND-LINE: --fmf-bound --no-cegqi -q
 ; EXPECT: sat
 (set-logic ALL)
 (assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
index 7f3a5b28f..8c72672cd 100644
--- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
+++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2
index 378380779..d32c1730e 100644
--- a/test/regress/regress1/fmf/loopy_coda.smt2
+++ b/test/regress/regress1/fmf/loopy_coda.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
index b2c42d7c5..3d30ae058 100644
--- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
index 5d1289997..7577e3966 100644
--- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
+++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 OPTION "produce-models";
 OPTION "fmf-bound";
diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2
index 25851f6e0..73de1a36f 100644
--- a/test/regress/regress1/fmf/nun-0208-to.smt2
+++ b/test/regress/regress1/fmf/nun-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort b__ 0)
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
index 841d050a7..25662d6eb 100644
--- a/test/regress/regress1/ho/issue4065-no-rep.smt2
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic AUFBV)
 (set-info :status sat)
 (set-option :bv-div-zero-const false)
diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
index 500ef6d4c..8846fe7fa 100644
--- a/test/regress/regress1/quantifiers/issue5470-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic NIA)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
index 9e8cd6586..d45d72253 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
index e9883297e..c7ef2d053 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
index 2c42744ac..17028065c 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
index f24aa6b1b..95608c150 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
index dbb653351..151499d78 100644
--- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2
index 01b633d8e..f985961df 100644
--- a/test/regress/regress1/sets/is_singleton1.smt2
+++ b/test/regress/regress1/sets/is_singleton1.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun S () (Set Int))
@@ -6,4 +8,4 @@
 (assert (= (singleton x) S))
 (assert (is_singleton S))
 (assert (is_singleton (singleton 3)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2
index ba8180b5e..75ac15817 100644
--- a/test/regress/regress1/sets/issue5271.smt2
+++ b/test/regress/regress1/sets/issue5271.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun s () (Set Int))
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc
index 4cac9a24e..194129518 100644
--- a/test/regress/regress1/sets/sets-tuple-poly.cvc
+++ b/test/regress/regress1/sets/sets-tuple-poly.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
diff --git a/test/regress/regress1/sets/univ-set-uf-elim.smt2 b/test/regress/regress1/sets/univ-set-uf-elim.smt2
index a22f2a44f..f02788a72 100644
--- a/test/regress/regress1/sets/univ-set-uf-elim.smt2
+++ b/test/regress/regress1/sets/univ-set-uf-elim.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --produce-models
 ; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
 ; EXIT: 1
 (set-logic ALL)
diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
index 78035790b..fd2060942 100644
--- a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
+++ b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
 (set-logic ALL)
 (declare-fun a () Int)
 (declare-fun b () Int)
diff --git a/test/regress/regress1/trim.cvc b/test/regress/regress1/trim.cvc
index 8bdbde79a..019b7702f 100644
--- a/test/regress/regress1/trim.cvc
+++ b/test/regress/regress1/trim.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find -q
 % EXPECT: sat
 DATATYPE
 	myType = A | B
diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2
index 54dfa0946..234e82229 100644
--- a/test/regress/regress2/bv_to_int_5095_2.smt2
+++ b/test/regress/regress2/bv_to_int_5095_2.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
-; COMMAND --solve-bv-as-int=sum
+; COMMAND-LINE: --solve-bv-as-int=sum -q
 (set-logic BV)
 (declare-const bv_42-0 (_ BitVec 42))
 (assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 938aa01ea..b688d3fcf 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)
 (set-option :finite-model-find true)