From 8f50a5600e0664330128d2ac824092a685ef965e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Apr 2021 20:45:01 -0500 Subject: [PATCH] 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. --- src/theory/theory_model.cpp | 35 ++++++++++++++----- test/regress/CMakeLists.txt | 3 +- .../regress/regress0/arith/div-chainable.smt2 | 2 +- test/regress/regress0/arith/issue3413.smt2 | 2 +- test/regress/regress0/bug484.smt2 | 2 +- .../regress/regress0/bv/bv_to_int_5293_2.smt2 | 2 +- test/regress/regress0/decision/quant-ex1.smt2 | 2 +- .../regress0/fmf/QEpres-uf.855035.smtv1.smt2 | 2 +- .../regress0/fmf/fmc_unsound_model.smt2 | 2 +- .../regress0/fmf/sc_bad_model_1221.smt2 | 2 +- test/regress/regress0/fp/issue3619.smt2 | 2 +- .../push-pop/real-as-int-incremental.smt2 | 2 +- .../quantifiers/horn-ground-pre-post.smt2 | 2 +- .../quantifiers/issue2033-macro-arith.smt2 | 2 +- .../quantifiers/macro-back-subs-sat.smt2 | 2 +- .../arith/issue4985-model-success.smt2 | 2 +- .../arith/issue4985b-model-success.smt2 | 2 +- .../regress1/fmf/Hoare-z3.931718.smtv1.smt2 | 2 +- .../regress1/fmf/LeftistHeap.scala-8-ncm.smt2 | 2 +- test/regress/regress1/fmf/am-bad-model.cvc | 2 +- test/regress/regress1/fmf/german169.smt2 | 2 +- test/regress/regress1/fmf/issue3626.smt2 | 2 +- .../regress1/fmf/jasmin-cdt-crash.smt2 | 2 +- test/regress/regress1/fmf/loopy_coda.smt2 | 2 +- .../regress1/fmf/lst-no-self-rev-exp.smt2 | 2 +- .../regress1/fmf/memory_model-R_cpp-dd.cvc | 2 +- test/regress/regress1/fmf/nun-0208-to.smt2 | 2 +- test/regress/regress1/fmf/refcount24.cvc.smt2 | 2 +- .../regress1/quantifiers/horn-simple.smt2 | 2 +- ...ction-example-onelane.proof-node22337.smt2 | 2 +- .../regress1/quantifiers/issue3664.smt2 | 2 +- .../regress1/quantifiers/issue4849-nqe.smt2 | 2 +- .../regress1/quantifiers/issue5470-aext.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvudiv-0.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvudiv-1.smt2 | 2 +- .../qbv-test-invert-bvurem-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvurem-1.smt2 | 2 +- .../quantifiers/qbv-test-urem-rewrite.smt2 | 2 +- test/regress/regress1/sets/is_singleton1.smt2 | 2 +- test/regress/regress1/sets/issue5271.smt2 | 2 +- .../regress/regress1/sets/sets-tuple-poly.cvc | 2 +- .../issue3657-unexpectedUnsatCVC4.smt2 | 5 ++- .../regress1/sygus/issue3944-div-rewrite.smt2 | 2 +- test/regress/regress1/trim.cvc | 2 +- .../regress2/issue3687-check-models.smt2 | 2 +- .../quantifiers/net-policy-no-time.smt2 | 2 +- .../sygus/issue4022-conjecture-gen.smt2 | 2 +- 47 files changed, 77 insertions(+), 54 deletions(-) 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::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) -- 2.30.2