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 d894ca571ed7b54c4bf856f22ed76e9eb97ad858..40a64cb3529d7707779e47f788b5a1aab927b031 100644 (file)
--- 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 cbe62c26d554165502d041ca7ac7c8b8c80165d7..08bdaf6eba64061ffcf7e8d24c5751c8439ba678 100644 (file)
--- 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 90aca07c3a9a2ccb9264538949191f3202bb16c0..ac2fb2352c38e88a10bc7746ddcc86c7400a7b56 100644 (file)
--- 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 c871226cea83ce64a93220eb0b79b5929dbde0de..080b25cde6f39a2d8e012b770760dd7677324590 100644 (file)
--- 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 e4bac6a0a89f9b954600871fee039968850da95d..ee7e1851655506d5f6f917b3dbc3cf2635703b21 100644 (file)
--- 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 1f812a503a20415217fae600760380cea69c4641..74cac05447ca16f26b4ab30ddbc3af3b3be369a3 100644 (file)
--- 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 3bb3d59995b59b675ddfcbaa53cfed5ed80cb45a..6fd9416d71d9490e7a4b56874b73d1f924028983 100644 (file)
--- 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 32a75e846c0392c2efadc05c348eba42c85f78df..619779c78a60de91eae906d669573f91d8d1e68f 100644 (file)
--- 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 5d0d8f6e6b6d4a34e11cb16a6913a82c5989ea48..e4e1f65b48d3a8fd4414a6e75648262fd88ebff7 100644 (file)
--- 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 890e765aa5102ef86f0303b2214b3c067d4ca223..d951e6c5045ba44a7cf1f1e3bb5178feec4b5cf0 100644 (file)
--- 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 3e0858035eafa36be1795cac6ec5d244b60eb632..55269e123fc63ffc23c52a616e58a0ffa5ae4371 100644 (file)
--- 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 155033d7db17fb7f82531437cf67cfb42662daf4..81af8c4e7765713c60938df382cca7da36f7d4e5 100644 (file)
--- 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 3a4f24521a3ba3cd1f27b4c989cdbf2c2cbfb61b..082df249bc2874be8740c86390510a31ed86a38b 100644 (file)
--- 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 d65a92aa5bfbcf87a080fad34f25d54eb91020bf..7993910fd527a4612e6747ce5d96f4d6bbeb1d32 100644 (file)
--- 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 bdb389a6365859651caae710cac7622435df3718..34b7422a5b8fd1073db2651ab79e88b69dd304a8 100644 (file)
--- 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 0249462ee5f9a43e8bdcfad4b50c5f73e6d1c17a..66a5a65829d3cd602e2dd9ef6f932b42cbf5c1e7 100644 (file)
--- 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 22b55c87f07b6e2c0358d5c85316ef11835f3f7a..3022e9da951eab3b473d53131cff61e94caab1cd 100644 (file)
--- 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 0bc9fe2bb7a5e6e827cb6d6daaea78b5f958ea42..8ee89145bb5b1571130e22a3486b9bbca28583ee 100644 (file)
--- 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 33c1796f95d14dc32d0205f8b9f83f62add16687..f1d20befc71f3af85d8eea69f0bc147d1eab5379 100644 (file)
--- 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 75d4e9f3dc499dd1a8fcbc7cfa9033174141e3cf..66be7e66f1a39a0fa44d6ffe1e3ed30600cd1d19 100644 (file)
--- 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 4bf21d53320bd608faab22fc1f8e833ef78a3141..c4a40ccc1ab324a2644714df0c529b2f6f91782d 100644 (file)
--- 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 6162b4cfe3e38bac1049fb545cc0d825f8beae4f..25dc80223156535656ed6a6dbe67989f0e0588be 100644 (file)
--- 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 8c72672cdb4b0e2a76896446c788a3139629fa8b..7f3a5b28fb712d256d9ace865e3a5226f4be1a4d 100644 (file)
--- 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 d32c1730ea6ef55f5686c142b36ab2492ab32bb0..37838077954728e257ea5d79f5fa707b1ecc18a0 100644 (file)
--- 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 3d30ae058d27122136d70f26f307060e9a2533a4..b2c42d7c54eb6632c74949a589925c1931ef5186 100644 (file)
--- 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 7577e3966bc17df3480f12b8dda60d2fb2efac6e..19930e6cac1af9e3402563a3b12a8460bcdb9941 100644 (file)
--- 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 73de1a36f790f9652aa3d3e3b88aab4535141db9..25851f6e0582fe00fad5949b56c6ceb6be0e2de7 100644 (file)
--- 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 510e5c4db9a01624507e91f8d9f18228330b7211..75bf893806cff1ed5b321a26ea9c5c35e2cbd323 100644 (file)
--- 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 d333358ed5986b30561bc15718c67c93b6bb696d..b851d2e19fcb233c5d8c1524a87cd17fb53da1fa 100644 (file)
--- 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 585ea0602d29f0784ad935a3502f6697d546a647..fdbac9996083e68a67db91fa43e548076e90f06b 100644 (file)
--- 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 0120f0e8a4cbbd8ae6f8d541ecf04621e0568eb9..28e9996045d7f49eb3c965aba03bac6e678943a8 100644 (file)
--- 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 dd7a22e39909af9b47e94db4d66605fd7776749e..4d0ce13fd8b8e913b65b47269311505871f0928b 100644 (file)
--- 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 8846fe7fa3216c61ad7bf3aa40527cfbb5d7e566..f414f46310c70072bffd3540292ec2f7e7b97f37 100644 (file)
--- 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 d45d72253d1ad74601c7c5dadd39255f6121c736..9e8cd65868f391ae25743eaffcda94cb0406f2e1 100644 (file)
--- 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 2935de44d5874999106664c2938c4cbeb1a83a8c..af4d006c984c87d1b724f93acc45acdb7c82b186 100644 (file)
--- 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 17028065c34672737f96c326d1b1374b654d22d0..2c42744ac12db6ef2bbeca9bbf29cf97a0f7b368 100644 (file)
--- 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 95608c15065727ae25fae31f370d21b5f2f7d856..f24aa6b1b2cdcd124978266264cfd11ceb38c872 100644 (file)
--- 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 151499d7822486151b9ea6965079e6c65f50bcfc..dbb653351e4777ef2eaf3c8ecaacfed0c3a09642 100644 (file)
--- 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 f985961dffe15acdcfad1999f06cf237f9f70ef4..5764a7d45bb3a7f704c083a02df00c370645015a 100644 (file)
--- 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 75ac15817857d4e7a2e03da85f12029442f51bdf..3c64e1d30dd8d6b2b83adfac73905eb4823f52a9 100644 (file)
--- 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 19412951840c6f307258b8b70e34ba9946c1ef8a..3f8662ef7d069d1d5a5b27c9b478e03d5267e9fd 100644 (file)
--- 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 648d436bb512ca052d50b9d61ac2dde9bdd071f1..0fc0e8b53594864dfd1432506f723be496fc8c60 100644 (file)
--- 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\r
+; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i --no-check-models\r
 ; EXPECT: sat\r
 ; EXPECT: sat\r
 ; EXPECT: sat\r
@@ -10,6 +10,9 @@
 ; EXPECT: sat\r
 ; EXPECT: sat\r
 ; EXPECT: sat\r
+\r
+; note that fmf-fun-rlv is incompatible with check-models\r
+\r
 (set-info :smt-lib-version 2.6)\r
 (set-option :produce-models true)\r
 (set-logic ALL)\r

diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
index fd20609427a86d98245b9a3bd59d9b7ddec490c4..78035790b0830ea1aeb2d15732831b405399aed6 100644 (file)
--- 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 019b7702fd6c623f9b1e90f2d284654f5f4da6ad..8bdbde79ab82a70c47b9055f006025e49d1e20a2 100644 (file)
--- 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 5c4155b83cfaabbfaecb147796ea62da3e928314..02f7754cf33c552e5495444a64f0076a66d8fc94 100644 (file)
--- 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 b688d3fcf57e6bfa2940af596962ce3220b6a09e..162ea0ad1f940720b242ecf45965b690dae6c076 100644 (file)
--- 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 6d0b37a305afe5a0c9086542cf24022af520f93d..1e77e88f3498d93df409b68d63aa8f1cd86c6339 100644 (file)
--- 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)