From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 24 Apr 2021 01:45:01 +0000 (-0500)
Subject: Improve getValue for non-evaluated operators (#6436)
X-Git-Tag: cvc5-1.0.0~1838
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f50a5600e0664330128d2ac824092a685ef965e;p=cvc5.git

Improve getValue for non-evaluated operators (#6436)

This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.

This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
---

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index d894ca571..40a64cb35 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -200,10 +200,13 @@ Node TheoryModel::getModelValue(TNode n) const
   Node ret = n;
   NodeManager* nm = NodeManager::currentNM();
 
-  // if it is an evaluated kind, compute model values for children and evaluate
-  if (n.getNumChildren() > 0
-      && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
-      && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end())
+  // If it has children, evaluate them. We do this even if n is an unevaluatable
+  // or semi-unevaluatable operator. Notice this includes quantified
+  // formulas. It may not be possible in general to evaluate bodies of
+  // quantified formulas, because they have free variables. Regardless, we
+  // may often be able to evaluate the body of a quantified formula to true,
+  // e.g. forall x. P(x) where P = lambda x. true.
+  if (n.getNumChildren() > 0)
   {
     Debug("model-getvalue-debug")
         << "Get model value children " << n << std::endl;
@@ -219,9 +222,17 @@ Node TheoryModel::getModelValue(TNode n) const
       children.push_back(n.getOperator());
     }
     // evaluate the children
-    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
     {
-      ret = getModelValue(n[i]);
+      if (n.isClosure() && i==0)
+      {
+        // do not evaluate bound variable lists
+        ret = n[0];
+      }
+      else
+      {
+        ret = getModelValue(n[i]);
+      }
       Debug("model-getvalue-debug")
           << "  " << n << "[" << i << "] is " << ret << std::endl;
       children.push_back(ret);
@@ -245,8 +256,16 @@ Node TheoryModel::getModelValue(TNode n) const
       ret = nm->mkConst(
           Rational(getCardinality(ret[0].getType()).getFiniteCardinality()));
     }
-    d_modelCache[n] = ret;
-    return ret;
+    // if the value was constant, we return it. If it was non-constant,
+    // we only return it if we an evaluated kind. This can occur if the
+    // children of n failed to evaluate.
+    if (ret.isConst() || (
+     d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
+      && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end()))
+    {
+      d_modelCache[n] = ret;
+      return ret;
+    }
   }
   // it might be approximate
   std::map<Node, Node>::const_iterator ita = d_approximations.find(n);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cbe62c26d..08bdaf6eb 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1532,7 +1532,6 @@ set(regress_1_tests
   regress1/fmf/issue5738-dt-interp-finite.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
-  regress1/fmf/ko-bound-set.cvc
   regress1/fmf/loopy_coda.smt2
   regress1/fmf/lst-no-self-rev-exp.smt2
   regress1/fmf/memory_model-R_cpp-dd.cvc
@@ -2548,6 +2547,8 @@ set(regression_disabled_tests
   ###
   regress1/bug472.smt2
   regress1/datatypes/non-simple-rec-set.smt2
+  # TODO: fix models (projects #276)
+  regress1/fmf/ko-bound-set.cvc
   # results in an assertion failure (see issue #1650).
   regress1/ho/hoa0102.smt2
   # slow on some builds after changes to tangent planes
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 90aca07c3..ac2fb2352 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2
index c871226ce..080b25cde 100644
--- a/test/regress/regress0/arith/issue3413.smt2
+++ b/test/regress/regress0/arith/issue3413.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_NIA)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
index e4bac6a0a..ee7e18516 100644
--- a/test/regress/regress0/bug484.smt2
+++ b/test/regress/regress0/bug484.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 
 ; Preamble  --------------
diff --git a/test/regress/regress0/bv/bv_to_int_5293_2.smt2 b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
index 1f812a503..74cac0544 100644
--- a/test/regress/regress0/bv/bv_to_int_5293_2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :solve-bv-as-int sum)
diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2
index 3bb3d5999..6fd9416d7 100644
--- a/test/regress/regress0/decision/quant-ex1.smt2
+++ b/test/regress/regress0/decision/quant-ex1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --decision=justification -q
+; COMMAND-LINE: --decision=justification
 ; EXPECT: sat
 
 (set-logic AUFLIRA)
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
index 32a75e846..619779c78 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-option :incremental false)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
index 5d0d8f6e6..e4e1f65b4 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 -q
+; COMMAND-LINE: --finite-model-find
 ; 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 890e765aa..d951e6c50 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 -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2
index 3e0858035..55269e123 100644
--- a/test/regress/regress0/fp/issue3619.smt2
+++ b/test/regress/regress0/fp/issue3619.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_FPLRA)
 (set-info :status sat)
diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
index 155033d7d..81af8c4e7 100644
--- a/test/regress/regress0/push-pop/real-as-int-incremental.smt2
+++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --solve-real-as-int -q
+; COMMAND-LINE: --incremental --solve-real-as-int
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
index 3a4f24521..082df249b 100644
--- a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
+++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inference -q
+; COMMAND-LINE: --sygus-inference
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
index d65a92aa5..7993910fd 100644
--- a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
+++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant -q
+; COMMAND-LINE: --macros-quant
 ; EXPECT: sat
 (set-logic AUFNIRA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
index bdb389a63..34b7422a5 100644
--- a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
+++ b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant -q
+; COMMAND-LINE: --macros-quant
 ; EXPECT: sat
 (set-logic UFLIA)
 (declare-fun A (Int) Int)
diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2
index 0249462ee..66a5a6582 100644
--- a/test/regress/regress1/arith/issue4985-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985-model-success.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2
index 22b55c87f..3022e9da9 100644
--- a/test/regress/regress1/arith/issue4985b-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985b-model-success.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
index 0bc9fe2bb..8ee89145b 100644
--- a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
+++ b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-option :incremental false)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
index 33c1796f9..f1d20befc 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 -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/am-bad-model.cvc b/test/regress/regress1/fmf/am-bad-model.cvc
index 75d4e9f3d..66be7e66f 100644
--- a/test/regress/regress1/fmf/am-bad-model.cvc
+++ b/test/regress/regress1/fmf/am-bad-model.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: -q
+% COMMAND-LINE:
 % EXPECT: sat
 OPTION "produce-models";
 OPTION "finite-model-find";
diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2
index 4bf21d533..c4a40ccc1 100644
--- a/test/regress/regress1/fmf/german169.smt2
+++ b/test/regress/regress1/fmf/german169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; 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 6162b4cfe..25dc80223 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 -q
+; COMMAND-LINE: --fmf-bound --no-cegqi
 ; 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 8c72672cd..7f3a5b28f 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 -q
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
 ; 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 d32c1730e..378380779 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 -q
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
 ; 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 3d30ae058..b2c42d7c5 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 -q
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
 ; 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 7577e3966..19930e6ca 100644
--- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
+++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: -q
+% COMMAND-LINE:
 % 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 73de1a36f..25851f6e0 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 -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort b__ 0)
diff --git a/test/regress/regress1/fmf/refcount24.cvc.smt2 b/test/regress/regress1/fmf/refcount24.cvc.smt2
index 510e5c4db..75bf89380 100644
--- a/test/regress/regress1/fmf/refcount24.cvc.smt2
+++ b/test/regress/regress1/fmf/refcount24.cvc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
index d333358ed..b851d2e19 100644
--- a/test/regress/regress1/quantifiers/horn-simple.smt2
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer -q
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
index 585ea0602..fdbac9996 100644
--- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
+++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv -q
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2
index 0120f0e8a..28e999604 100644
--- a/test/regress/regress1/quantifiers/issue3664.smt2
+++ b/test/regress/regress1/quantifiers/issue3664.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun-rlv --sygus-inference -q
+; COMMAND-LINE: --fmf-fun-rlv --sygus-inference
 ; EXPECT: sat
 (set-logic QF_NRA)
 (declare-fun a () Real)
diff --git a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 b/test/regress/regress1/quantifiers/issue4849-nqe.smt2
index dd7a22e39..4d0ce13fd 100644
--- a/test/regress/regress1/quantifiers/issue4849-nqe.smt2
+++ b/test/regress/regress1/quantifiers/issue4849-nqe.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-nested-qe -q
+; COMMAND-LINE: --cegqi-nested-qe
 ; EXPECT: sat
 (set-logic LIA)
 (set-option :cegqi-nested-qe true)
diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
index 8846fe7fa..f414f4631 100644
--- a/test/regress/regress1/quantifiers/issue5470-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic NIA)
 (set-option :strings-exp true)
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 d45d72253..9e8cd6586 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 -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; 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 2935de44d..af4d006c9 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 -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; 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 17028065c..2c42744ac 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 -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; 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 95608c150..f24aa6b1b 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 -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; 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 151499d78..dbb653351 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 -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; 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 f985961df..5764a7d45 100644
--- a/test/regress/regress1/sets/is_singleton1.smt2
+++ b/test/regress/regress1/sets/is_singleton1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2
index 75ac15817..3c64e1d30 100644
--- a/test/regress/regress1/sets/issue5271.smt2
+++ b/test/regress/regress1/sets/issue5271.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc
index 194129518..3f8662ef7 100644
--- a/test/regress/regress1/sets/sets-tuple-poly.cvc
+++ b/test/regress/regress1/sets/sets-tuple-poly.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: -q
+% COMMAND-LINE:
 % EXPECT: sat
 OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
diff --git a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
index 648d436bb..0fc0e8b53 100644
--- a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
+++ b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i -q
+; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i --no-check-models
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
@@ -10,6 +10,9 @@
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
+
+; note that fmf-fun-rlv is incompatible with check-models
+
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)
 (set-logic ALL)
diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
index fd2060942..78035790b 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 -q
+; COMMAND-LINE: --sygus-inference
 (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 019b7702f..8bdbde79a 100644
--- a/test/regress/regress1/trim.cvc
+++ b/test/regress/regress1/trim.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find -q
+% COMMAND-LINE: --finite-model-find
 % EXPECT: sat
 DATATYPE
 	myType = A | B
diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
index 5c4155b83..02f7754cf 100644
--- a/test/regress/regress2/issue3687-check-models.smt2
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --check-models -q
+; COMMAND-LINE: --check-models
 ; EXPECT: sat
 (set-logic QF_ABV)
 (declare-fun c () (_ BitVec 32))
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index b688d3fcf..162ea0ad1 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)
diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
index 6d0b37a30..1e77e88f3 100644
--- a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
+++ b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :conjecture-filter-model true)