From 18be156d626248e8c0b125e98f4aac059fa085c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 May 2022 14:28:52 -0500 Subject: [PATCH] Improvements for evaluation in model (#8738) This marks APPLY_SELECTOR and SEQ_NTH as unevaluatable kinds. This means that get-value applied to applications of them e.g. (seq.nth t) will evaluate to c if (seq.nth t) is in the same equivalence class as constant c. (Note that this could be further improved to reason by congruence for (seq.nth s) where s = t, which I'm considering to do on a followup PR). This removes many of the required -q from the command line arguments of our regressions. This also does some minor cleanup to our regressions to remove -q from further regressions. --- src/theory/datatypes/theory_datatypes.cpp | 2 ++ src/theory/strings/theory_strings.cpp | 2 ++ src/theory/theory_model.cpp | 14 ++++++-------- test/regress/cli/regress0/arith/div.05.smt2 | 1 - .../cli/regress0/arith/issue7984-quant-trans.smt2 | 1 - .../regress0/arith/projissue469-int-equality.smt2 | 2 +- test/regress/cli/regress0/cores/issue3455.smt2 | 3 ++- test/regress/cli/regress0/cores/issue3651.smt2 | 3 ++- test/regress/cli/regress0/cores/issue4971-0.smt2 | 3 ++- test/regress/cli/regress0/cores/issue4971-1.smt2 | 5 +++-- test/regress/cli/regress0/cores/issue4971-3.smt2 | 3 ++- test/regress/cli/regress0/cores/issue5902.smt2 | 2 +- test/regress/cli/regress0/cores/issue5908.smt2 | 5 +++-- .../cli/regress0/datatypes/data-nested-codata.smt2 | 1 - .../cli/regress0/datatypes/datatype1.cvc.smt2 | 1 - .../cli/regress0/datatypes/datatype3.cvc.smt2 | 1 - test/regress/cli/regress0/datatypes/issue1433.smt2 | 1 - .../cli/regress0/datatypes/issue2838.cvc.smt2 | 1 - .../datatypes/parametric-alt-list.cvc.smt2 | 1 - .../cli/regress0/datatypes/v3l60006.cvc.smt2 | 1 - .../cli/regress0/datatypes/wrong-sel-simp.cvc.smt2 | 1 - test/regress/cli/regress0/fp/issue3536.smt2 | 1 - test/regress/cli/regress0/fp/issue3619.smt2 | 1 - .../cli/regress0/fp/issue4277-assign-func.smt2 | 1 - test/regress/cli/regress0/issue5099-model-2.smt2 | 2 +- test/regress/cli/regress0/issue5473.smt2 | 1 - test/regress/cli/regress0/issue5736.smt2 | 2 +- test/regress/cli/regress0/issue5743.smt2 | 1 - test/regress/cli/regress0/issue5947.smt2 | 1 - .../nl/nta/issue4693-4-inc-purify-sat.smt2 | 2 +- .../regress0/nl/nta/issue4693-5-inc-purify.smt2 | 1 - .../cli/regress0/nl/nta/issue4693-inc-purify.smt2 | 2 +- .../regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 | 1 - .../parser/issue7894-parse-error-assoc.smt2 | 2 +- test/regress/cli/regress0/parser/to_fp.smt2 | 2 +- .../regress0/quantifiers/issue8001-mem-leak.smt2 | 2 +- .../cli/regress0/quantifiers/pure_dt_cbqi.smt2 | 2 +- .../cli/regress0/seq/mixed-types-seq-nth.smt2 | 2 +- test/regress/cli/regress0/seq/nth-update.smt2 | 2 +- test/regress/cli/regress0/seq/seq-expand-defs.smt2 | 4 ++-- test/regress/cli/regress0/seq/seq-nth.smt2 | 2 +- .../cli/regress0/seq/update-concat-non-atomic.smt2 | 2 +- .../regress0/seq/update-concat-non-atomic2.smt2 | 2 +- .../cli/regress0/seq/wrong-model-020322.smt2 | 2 +- test/regress/cli/regress1/bug507.smt2 | 1 - test/regress/cli/regress1/bug516.smt2 | 2 +- .../regress/cli/regress1/cee-bug0909-dd-scope.smt2 | 4 ++-- test/regress/cli/regress1/cores/issue5604.smt2 | 3 ++- .../regress1/datatypes/non-simple-rec-param.smt2 | 2 +- test/regress/cli/regress1/fmf/bug651.smt2 | 3 ++- .../regress/cli/regress1/fmf/cons-sets-bounds.smt2 | 2 +- .../regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 | 2 +- test/regress/cli/regress1/fmf/loopy_coda.smt2 | 2 +- .../cli/regress1/fmf/lst-no-self-rev-exp.smt2 | 2 +- test/regress/cli/regress1/fmf/nun-0208-to.smt2 | 2 +- test/regress/cli/regress1/fmf/pow2-bool.smt2 | 3 ++- .../regress1/nl/transcedental_model_simple.smt2 | 2 +- .../cli/regress1/quantifiers/issue5484-qe.smt2 | 1 - .../cli/regress1/quantifiers/issue5484b-qe.smt2 | 1 - .../regress1/quantifiers/qbv-simple-2vars-vo.smt2 | 2 +- .../cli/regress1/quantifiers/qbv-subcall.smt2 | 1 - .../regress1/quantifiers/smtcomp-qbv-053118.smt2 | 1 - .../cli/regress1/seq/issue8148-2-const-mv.smt2 | 2 +- .../cli/regress1/seq/issue8148-const-mv.smt2 | 2 +- test/regress/cli/regress1/strings/issue1105.smt2 | 1 - test/regress/cli/regress1/strings/issue6913.smt2 | 2 +- .../cli/regress1/wrong-qfabvfp-smtcomp2018.smt2 | 4 ++-- test/regress/cli/regress2/bug765.smt2 | 3 ++- .../regress2/quantifiers/net-policy-no-time.smt2 | 1 - test/regress/cli/regress2/strings/issue6483.smt2 | 1 - 70 files changed, 66 insertions(+), 80 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 5824b46cf..19f18fde5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -122,6 +122,8 @@ void TheoryDatatypes::finishInit() // testers are not relevant for model building d_valuation.setIrrelevantKind(APPLY_TESTER); d_valuation.setIrrelevantKind(DT_SYGUS_BOUND); + // selectors don't always evaluate + d_valuation.setUnevaluatedKind(APPLY_SELECTOR); } TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e1627de97..73d790200 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -162,6 +162,8 @@ void TheoryStrings::finishInit() // memberships are not relevant for model building d_valuation.setIrrelevantKind(kind::STRING_IN_REGEXP); + // seq nth doesn't always evaluate + d_valuation.setUnevaluatedKind(SEQ_NTH); } std::string TheoryStrings::identify() const diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 52ff94510..6465743c1 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -260,7 +260,7 @@ Node TheoryModel::getModelValue(TNode n) const <= cc.getUpperBound()); } // 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 + // we only return it if we are 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() @@ -269,12 +269,15 @@ Node TheoryModel::getModelValue(TNode n) const d_modelCache[n] = ret; return ret; } + // Note that we discard the evaluation of the arguments here + Trace("model-getvalue-debug") << "Failed to evaluate " << ret << std::endl; } // must rewrite the term at this point ret = rewrite(n); + Trace("model-getvalue-debug") + << "Look up " << ret << " in equality engine" << std::endl; // return the representative of the term in the equality engine, if it exists TypeNode t = ret.getType(); - bool eeHasTerm; if (!logicInfo().isHigherOrder() && (t.isFunction() || t.isPredicate())) { // functions are in the equality engine, but *not* as first-class members @@ -283,13 +286,8 @@ Node TheoryModel::getModelValue(TNode n) const // to the equality engine despite hasTerm returning true. However, they are // first class members when higher-order is enabled. Hence, the special // case here. - eeHasTerm = false; - } - else - { - eeHasTerm = d_equalityEngine->hasTerm(ret); } - if (eeHasTerm) + else if (d_equalityEngine->hasTerm(ret)) { Trace("model-getvalue-debug") << "get value from representative " << ret << "..." << std::endl; diff --git a/test/regress/cli/regress0/arith/div.05.smt2 b/test/regress/cli/regress0/arith/div.05.smt2 index 0342fc90c..99e6b04d5 100644 --- a/test/regress/cli/regress0/arith/div.05.smt2 +++ b/test/regress/cli/regress0/arith/div.05.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_NRA) (set-info :smt-lib-version 2.6) diff --git a/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 b/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 index b0de9c7a5..e6d5d1b3a 100644 --- a/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 +++ b/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 b/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 index 59fdf1d48..e8bffa564 100644 --- a/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 +++ b/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: -q ; EXPECT: sat +(set-logic ALL) (set-option :nl-ext-ent-conf true) (declare-const x Int) (assert (> (* x x) (+ x x))) diff --git a/test/regress/cli/regress0/cores/issue3455.smt2 b/test/regress/cli/regress0/cores/issue3455.smt2 index c07fc5541..57a556583 100644 --- a/test/regress/cli/regress0/cores/issue3455.smt2 +++ b/test/regress/cli/regress0/cores/issue3455.smt2 @@ -1,9 +1,10 @@ -; COMMAND-LINE: -q --incremental +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat +(set-logic ALL) (declare-fun x0 () Real) (check-sat) (assert (<= (* x0 (- 1.0)) 0.0)) diff --git a/test/regress/cli/regress0/cores/issue3651.smt2 b/test/regress/cli/regress0/cores/issue3651.smt2 index 478f198ab..39218bb07 100644 --- a/test/regress/cli/regress0/cores/issue3651.smt2 +++ b/test/regress/cli/regress0/cores/issue3651.smt2 @@ -1,9 +1,10 @@ -; COMMAND-LINE: --incremental -q +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat +(set-logic ALL) (declare-fun a () Real) (declare-fun b () Real) (declare-fun c () Real) diff --git a/test/regress/cli/regress0/cores/issue4971-0.smt2 b/test/regress/cli/regress0/cores/issue4971-0.smt2 index 254b8c3b3..df424b781 100644 --- a/test/regress/cli/regress0/cores/issue4971-0.smt2 +++ b/test/regress/cli/regress0/cores/issue4971-0.smt2 @@ -1,9 +1,10 @@ -; COMMAND-LINE: --incremental -q --cegqi-full --produce-unsat-cores +; COMMAND-LINE: --incremental --cegqi-full --produce-unsat-cores ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: ( ; EXPECT: IP_1 ; EXPECT: ) +(set-logic ALL) (declare-const v1 Bool) (declare-const v9 Bool) (declare-const v14 Bool) diff --git a/test/regress/cli/regress0/cores/issue4971-1.smt2 b/test/regress/cli/regress0/cores/issue4971-1.smt2 index fcbd5dbde..81f22b8be 100644 --- a/test/regress/cli/regress0/cores/issue4971-1.smt2 +++ b/test/regress/cli/regress0/cores/issue4971-1.smt2 @@ -1,7 +1,8 @@ -; COMMAND-LINE: --incremental -q --produce-unsat-cores -; COMMAND-LINE: --incremental -q --unsat-cores-mode=sat-proof --produce-unsat-cores +; COMMAND-LINE: --incremental --produce-unsat-cores +; COMMAND-LINE: --incremental --unsat-cores-mode=sat-proof --produce-unsat-cores ; EXPECT: sat ; EXPECT: sat +(set-logic ALL) (declare-const i2 Int) (declare-const i5 Int) (declare-fun st2 () (Set Int)) diff --git a/test/regress/cli/regress0/cores/issue4971-3.smt2 b/test/regress/cli/regress0/cores/issue4971-3.smt2 index 36495b5ed..8f889a1f8 100644 --- a/test/regress/cli/regress0/cores/issue4971-3.smt2 +++ b/test/regress/cli/regress0/cores/issue4971-3.smt2 @@ -1,8 +1,9 @@ -; COMMAND-LINE: --incremental -q --produce-unsat-cores +; COMMAND-LINE: --incremental --produce-unsat-cores ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat +(set-logic ALL) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const v3 Bool) diff --git a/test/regress/cli/regress0/cores/issue5902.smt2 b/test/regress/cli/regress0/cores/issue5902.smt2 index 3c930b26b..470ce3eb6 100644 --- a/test/regress/cli/regress0/cores/issue5902.smt2 +++ b/test/regress/cli/regress0/cores/issue5902.smt2 @@ -1,3 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: unsat +(set-logic ALL) (check-sat-assuming (false)) diff --git a/test/regress/cli/regress0/cores/issue5908.smt2 b/test/regress/cli/regress0/cores/issue5908.smt2 index 3224079ba..3d4d290a8 100644 --- a/test/regress/cli/regress0/cores/issue5908.smt2 +++ b/test/regress/cli/regress0/cores/issue5908.smt2 @@ -1,7 +1,8 @@ -; COMMAND-LINE: -i -q +; COMMAND-LINE: -i ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat +(set-logic ALL) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) @@ -19,4 +20,4 @@ (pop) (assert (> e a)) (assert (= e 0)) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/cli/regress0/datatypes/data-nested-codata.smt2 b/test/regress/cli/regress0/datatypes/data-nested-codata.smt2 index d49f47427..5fc0daf98 100644 --- a/test/regress/cli/regress0/datatypes/data-nested-codata.smt2 +++ b/test/regress/cli/regress0/datatypes/data-nested-codata.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_DTLIA) (set-info :status sat) diff --git a/test/regress/cli/regress0/datatypes/datatype1.cvc.smt2 b/test/regress/cli/regress0/datatypes/datatype1.cvc.smt2 index 387899b68..a7721f553 100644 --- a/test/regress/cli/regress0/datatypes/datatype1.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/datatype1.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/datatypes/datatype3.cvc.smt2 b/test/regress/cli/regress0/datatypes/datatype3.cvc.smt2 index 68db235de..06c241e74 100644 --- a/test/regress/cli/regress0/datatypes/datatype3.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/datatype3.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/datatypes/issue1433.smt2 b/test/regress/cli/regress0/datatypes/issue1433.smt2 index edbd6da69..e70d8a897 100644 --- a/test/regress/cli/regress0/datatypes/issue1433.smt2 +++ b/test/regress/cli/regress0/datatypes/issue1433.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_UFDTLIA) (set-info :status sat) diff --git a/test/regress/cli/regress0/datatypes/issue2838.cvc.smt2 b/test/regress/cli/regress0/datatypes/issue2838.cvc.smt2 index 8693f0fd6..cb4a2161b 100644 --- a/test/regress/cli/regress0/datatypes/issue2838.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/issue2838.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/datatypes/parametric-alt-list.cvc.smt2 b/test/regress/cli/regress0/datatypes/parametric-alt-list.cvc.smt2 index a9694c623..2ea829b6c 100644 --- a/test/regress/cli/regress0/datatypes/parametric-alt-list.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/parametric-alt-list.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/datatypes/v3l60006.cvc.smt2 b/test/regress/cli/regress0/datatypes/v3l60006.cvc.smt2 index 8906757a9..16df4e411 100644 --- a/test/regress/cli/regress0/datatypes/v3l60006.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/v3l60006.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/datatypes/wrong-sel-simp.cvc.smt2 b/test/regress/cli/regress0/datatypes/wrong-sel-simp.cvc.smt2 index 1e8d52ff5..22b3e02a4 100644 --- a/test/regress/cli/regress0/datatypes/wrong-sel-simp.cvc.smt2 +++ b/test/regress/cli/regress0/datatypes/wrong-sel-simp.cvc.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/fp/issue3536.smt2 b/test/regress/cli/regress0/fp/issue3536.smt2 index 6a58b371f..7f79ddbaf 100644 --- a/test/regress/cli/regress0/fp/issue3536.smt2 +++ b/test/regress/cli/regress0/fp/issue3536.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FP) (declare-const x (_ FloatingPoint 11 53)) diff --git a/test/regress/cli/regress0/fp/issue3619.smt2 b/test/regress/cli/regress0/fp/issue3619.smt2 index ab3c781bb..a297bcfb0 100644 --- a/test/regress/cli/regress0/fp/issue3619.smt2 +++ b/test/regress/cli/regress0/fp/issue3619.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FPLRA) (set-info :status sat) diff --git a/test/regress/cli/regress0/fp/issue4277-assign-func.smt2 b/test/regress/cli/regress0/fp/issue4277-assign-func.smt2 index 33753375f..95e055efa 100644 --- a/test/regress/cli/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/cli/regress0/fp/issue4277-assign-func.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic HO_ALL) (set-option :assign-function-values false) diff --git a/test/regress/cli/regress0/issue5099-model-2.smt2 b/test/regress/cli/regress0/issue5099-model-2.smt2 index 9feada280..b045b809a 100644 --- a/test/regress/cli/regress0/issue5099-model-2.smt2 +++ b/test/regress/cli/regress0/issue5099-model-2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -m -q +; COMMAND-LINE: -m ; EXPECT: sat ; EXPECT: ((IP true)) (set-logic QF_NRA) diff --git a/test/regress/cli/regress0/issue5473.smt2 b/test/regress/cli/regress0/issue5473.smt2 index bf24726f9..0c150ba96 100644 --- a/test/regress/cli/regress0/issue5473.smt2 +++ b/test/regress/cli/regress0/issue5473.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat ; EXPECT: ((baz true)) (set-logic QF_NIRA) diff --git a/test/regress/cli/regress0/issue5736.smt2 b/test/regress/cli/regress0/issue5736.smt2 index e0244b419..82999e1ec 100644 --- a/test/regress/cli/regress0/issue5736.smt2 +++ b/test/regress/cli/regress0/issue5736.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -q +(set-logic ALL) (set-info :status sat) (declare-fun a () (Array (_ BitVec 32) (_ BitVec 32))) (declare-fun b () (Array (_ BitVec 32) (_ BitVec 32))) diff --git a/test/regress/cli/regress0/issue5743.smt2 b/test/regress/cli/regress0/issue5743.smt2 index 644723916..94425fb0a 100644 --- a/test/regress/cli/regress0/issue5743.smt2 +++ b/test/regress/cli/regress0/issue5743.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q (set-logic QF_AUFBV) (set-info :status sat) (declare-fun bv_22-0 () (_ BitVec 1)) diff --git a/test/regress/cli/regress0/issue5947.smt2 b/test/regress/cli/regress0/issue5947.smt2 index a5c736323..987c74938 100644 --- a/test/regress/cli/regress0/issue5947.smt2 +++ b/test/regress/cli/regress0/issue5947.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q (set-logic QF_UFBVLIA) (set-info :status sat) (declare-fun f ((_ BitVec 3)) Int) diff --git a/test/regress/cli/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 index 1b3ad0ab7..ee71ec4b2 100644 --- a/test/regress/cli/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -i -q --no-debug-check-models +; COMMAND-LINE: -i --no-debug-check-models ; EXPECT: sat ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 index 9acc326d0..0ae3b6f5a 100644 --- a/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2 index b9e8e61bf..181ace48d 100644 --- a/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -i -q +; COMMAND-LINE: -i ; EXPECT: unsat ; EXPECT: unsat (set-logic QF_NRAT) diff --git a/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 b/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 index c74d7ad6a..7aa977b6e 100644 --- a/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress0/parser/issue7894-parse-error-assoc.smt2 b/test/regress/cli/regress0/parser/issue7894-parse-error-assoc.smt2 index 1962c53e1..0505f4291 100644 --- a/test/regress/cli/regress0/parser/issue7894-parse-error-assoc.smt2 +++ b/test/regress/cli/regress0/parser/issue7894-parse-error-assoc.smt2 @@ -1,6 +1,6 @@ ; DISABLE-TESTER: dump -; COMMAND-LINE: -q ; SCRUBBER: grep -o "must have at least 2 children" ; EXPECT: must have at least 2 children ; EXIT: 1 +(set-logic ALL) (assert (= (+ 0))) diff --git a/test/regress/cli/regress0/parser/to_fp.smt2 b/test/regress/cli/regress0/parser/to_fp.smt2 index 1cd83816a..2e91ae91c 100644 --- a/test/regress/cli/regress0/parser/to_fp.smt2 +++ b/test/regress/cli/regress0/parser/to_fp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strict-parsing -q +; COMMAND-LINE: --strict-parsing ; EXPECT: sat (set-logic QF_FP) (declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24)) diff --git a/test/regress/cli/regress0/quantifiers/issue8001-mem-leak.smt2 b/test/regress/cli/regress0/quantifiers/issue8001-mem-leak.smt2 index 33695a7af..334ede9be 100644 --- a/test/regress/cli/regress0/quantifiers/issue8001-mem-leak.smt2 +++ b/test/regress/cli/regress0/quantifiers/issue8001-mem-leak.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -q ; EXPECT: unknown +(set-logic ALL) (assert (forall ((V (Array Int Int))) (= 0 (select V 0)))) (check-sat) diff --git a/test/regress/cli/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/cli/regress0/quantifiers/pure_dt_cbqi.smt2 index ece9532b4..764c2dbed 100644 --- a/test/regress/cli/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/cli/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi -q +; COMMAND-LINE: --cegqi ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress0/seq/mixed-types-seq-nth.smt2 b/test/regress/cli/regress0/seq/mixed-types-seq-nth.smt2 index 0577479fc..b2636bbb1 100644 --- a/test/regress/cli/regress0/seq/mixed-types-seq-nth.smt2 +++ b/test/regress/cli/regress0/seq/mixed-types-seq-nth.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --seq-array=lazy -q +; COMMAND-LINE: --seq-array=lazy (set-logic QF_UFSLIA) (declare-sort E 0) diff --git a/test/regress/cli/regress0/seq/nth-update.smt2 b/test/regress/cli/regress0/seq/nth-update.smt2 index 5c194ffad..7774eb752 100644 --- a/test/regress/cli/regress0/seq/nth-update.smt2 +++ b/test/regress/cli/regress0/seq/nth-update.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --seq-array=lazy -q +; COMMAND-LINE: --strings-exp --seq-array=lazy ; EXPECT: sat (set-logic QF_SLIA) (declare-const x (Seq Int)) diff --git a/test/regress/cli/regress0/seq/seq-expand-defs.smt2 b/test/regress/cli/regress0/seq/seq-expand-defs.smt2 index cafb516ba..3e51627c0 100644 --- a/test/regress/cli/regress0/seq/seq-expand-defs.smt2 +++ b/test/regress/cli/regress0/seq/seq-expand-defs.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ; EXPECT: sat -; EXPECT: (((seq.nth y 7) (seq.nth (as seq.empty (Seq Int)) 7))) +; EXPECT: (((seq.nth y 7) 404)) ; EXPECT: (((str.from_code x) "?")) (set-logic ALL) (set-option :produce-models true) diff --git a/test/regress/cli/regress0/seq/seq-nth.smt2 b/test/regress/cli/regress0/seq/seq-nth.smt2 index af637e2bc..3ff2ab096 100644 --- a/test/regress/cli/regress0/seq/seq-nth.smt2 +++ b/test/regress/cli/regress0/seq/seq-nth.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ;EXPECT: sat (set-logic ALL) (declare-fun s () (Seq Int)) diff --git a/test/regress/cli/regress0/seq/update-concat-non-atomic.smt2 b/test/regress/cli/regress0/seq/update-concat-non-atomic.smt2 index 346f9c45f..b7932042b 100644 --- a/test/regress/cli/regress0/seq/update-concat-non-atomic.smt2 +++ b/test/regress/cli/regress0/seq/update-concat-non-atomic.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --seq-array=lazy -q +; COMMAND-LINE: --strings-exp --seq-array=lazy ; EXPECT: sat (set-logic ALL) (declare-sort S 0) diff --git a/test/regress/cli/regress0/seq/update-concat-non-atomic2.smt2 b/test/regress/cli/regress0/seq/update-concat-non-atomic2.smt2 index 5c14a10cf..e4a581af9 100644 --- a/test/regress/cli/regress0/seq/update-concat-non-atomic2.smt2 +++ b/test/regress/cli/regress0/seq/update-concat-non-atomic2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --seq-array=lazy -q +; COMMAND-LINE: --strings-exp --seq-array=lazy ; EXPECT: sat (set-logic ALL) (declare-sort S 0) diff --git a/test/regress/cli/regress0/seq/wrong-model-020322.smt2 b/test/regress/cli/regress0/seq/wrong-model-020322.smt2 index 683761ef5..f9e622ad0 100644 --- a/test/regress/cli/regress0/seq/wrong-model-020322.smt2 +++ b/test/regress/cli/regress0/seq/wrong-model-020322.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --seq-array=lazy -q +; COMMAND-LINE: --strings-exp --seq-array=lazy ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/bug507.smt2 b/test/regress/cli/regress1/bug507.smt2 index fb6998d71..61732438b 100644 --- a/test/regress/cli/regress1/bug507.smt2 +++ b/test/regress/cli/regress1/bug507.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/bug516.smt2 b/test/regress/cli/regress1/bug516.smt2 index 19a500bed..2bf143012 100644 --- a/test/regress/cli/regress1/bug516.smt2 +++ b/test/regress/cli/regress1/bug516.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound -q +; COMMAND-LINE: --finite-model-find --fmf-bound ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/cli/regress1/cee-bug0909-dd-scope.smt2 index 5000dcb94..6ce621a98 100644 --- a/test/regress/cli/regress1/cee-bug0909-dd-scope.smt2 +++ b/test/regress/cli/regress1/cee-bug0909-dd-scope.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --ee-mode=distributed -q -; COMMAND-LINE: --ee-mode=central -q +; COMMAND-LINE: --ee-mode=distributed +; COMMAND-LINE: --ee-mode=central ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/cores/issue5604.smt2 b/test/regress/cli/regress1/cores/issue5604.smt2 index e41335a4a..d45eebdcb 100644 --- a/test/regress/cli/regress1/cores/issue5604.smt2 +++ b/test/regress/cli/regress1/cores/issue5604.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ; EXPECT: unsat +(set-logic ALL) (declare-fun a () String) (declare-fun b () String) (declare-fun c () String) diff --git a/test/regress/cli/regress1/datatypes/non-simple-rec-param.smt2 b/test/regress/cli/regress1/datatypes/non-simple-rec-param.smt2 index 345a67d73..8db92b0fd 100644 --- a/test/regress/cli/regress1/datatypes/non-simple-rec-param.smt2 +++ b/test/regress/cli/regress1/datatypes/non-simple-rec-param.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --dt-nested-rec -q +; COMMAND-LINE: --dt-nested-rec ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/fmf/bug651.smt2 b/test/regress/cli/regress1/fmf/bug651.smt2 index b9734b1e5..ce1f497b3 100644 --- a/test/regress/cli/regress1/fmf/bug651.smt2 +++ b/test/regress/cli/regress1/fmf/bug651.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --fmf-fun --fmf-bound -q +; COMMAND-LINE: --fmf-fun --fmf-bound ; EXPECT: sat +; DISABLE-TESTER: model (set-logic UFDTSLIA) (set-option :produce-models true) diff --git a/test/regress/cli/regress1/fmf/cons-sets-bounds.smt2 b/test/regress/cli/regress1/fmf/cons-sets-bounds.smt2 index c917d74d9..f0ff20de9 100644 --- a/test/regress/cli/regress1/fmf/cons-sets-bounds.smt2 +++ b/test/regress/cli/regress1/fmf/cons-sets-bounds.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound -q +; COMMAND-LINE: --fmf-bound ; EXPECT: sat (set-logic ALL) (declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil)))) diff --git a/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 index 2b9f93d60..ede231129 100644 --- a/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 +++ b/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q +; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/fmf/loopy_coda.smt2 b/test/regress/cli/regress1/fmf/loopy_coda.smt2 index 6b7b95230..5dd3f8824 100644 --- a/test/regress/cli/regress1/fmf/loopy_coda.smt2 +++ b/test/regress/cli/regress1/fmf/loopy_coda.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q +; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/cli/regress1/fmf/lst-no-self-rev-exp.smt2 index 4c06908dd..8dfb8cfca 100644 --- a/test/regress/cli/regress1/fmf/lst-no-self-rev-exp.smt2 +++ b/test/regress/cli/regress1/fmf/lst-no-self-rev-exp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find -q +; COMMAND-LINE: --finite-model-find ; EXPECT: sat (set-logic ALL) (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil)))) diff --git a/test/regress/cli/regress1/fmf/nun-0208-to.smt2 b/test/regress/cli/regress1/fmf/nun-0208-to.smt2 index f74b4b243..32974ef41 100644 --- a/test/regress/cli/regress1/fmf/nun-0208-to.smt2 +++ b/test/regress/cli/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) (declare-sort b__ 0) diff --git a/test/regress/cli/regress1/fmf/pow2-bool.smt2 b/test/regress/cli/regress1/fmf/pow2-bool.smt2 index b92aec228..c54d9ac9b 100644 --- a/test/regress/cli/regress1/fmf/pow2-bool.smt2 +++ b/test/regress/cli/regress1/fmf/pow2-bool.smt2 @@ -1,5 +1,6 @@ -; COMMAND-LINE: --fmf-fun -q +; COMMAND-LINE: --fmf-fun ; EXPECT: sat +; DISABLE-TESTER: model (set-logic ALL) (define-fun-rec p2 ((n Int) (p Int)) Bool ( diff --git a/test/regress/cli/regress1/nl/transcedental_model_simple.smt2 b/test/regress/cli/regress1/nl/transcedental_model_simple.smt2 index 473ac25bf..2930a3a74 100644 --- a/test/regress/cli/regress1/nl/transcedental_model_simple.smt2 +++ b/test/regress/cli/regress1/nl/transcedental_model_simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-rlv=always -q +; COMMAND-LINE: --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/cli/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/cli/regress1/quantifiers/issue5484-qe.smt2 index 9fcc7dcba..c6dead0ea 100644 --- a/test/regress/cli/regress1/quantifiers/issue5484-qe.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5484-qe.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 diff --git a/test/regress/cli/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/cli/regress1/quantifiers/issue5484b-qe.smt2 index 754603135..0e5be545e 100644 --- a/test/regress/cli/regress1/quantifiers/issue5484b-qe.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5484b-qe.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 diff --git a/test/regress/cli/regress1/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/cli/regress1/quantifiers/qbv-simple-2vars-vo.smt2 index f291ec0ec..31cc96325 100644 --- a/test/regress/cli/regress1/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/cli/regress1/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/cli/regress1/quantifiers/qbv-subcall.smt2 b/test/regress/cli/regress1/quantifiers/qbv-subcall.smt2 index 42a93921b..fd0908b5e 100644 --- a/test/regress/cli/regress1/quantifiers/qbv-subcall.smt2 +++ b/test/regress/cli/regress1/quantifiers/qbv-subcall.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/cli/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/cli/regress1/quantifiers/smtcomp-qbv-053118.smt2 index d8bb5fcaf..4483035dc 100644 --- a/test/regress/cli/regress1/quantifiers/smtcomp-qbv-053118.smt2 +++ b/test/regress/cli/regress1/quantifiers/smtcomp-qbv-053118.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic BV) diff --git a/test/regress/cli/regress1/seq/issue8148-2-const-mv.smt2 b/test/regress/cli/regress1/seq/issue8148-2-const-mv.smt2 index 7ef7f93db..c26a74f22 100644 --- a/test/regress/cli/regress1/seq/issue8148-2-const-mv.smt2 +++ b/test/regress/cli/regress1/seq/issue8148-2-const-mv.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 b/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 index f7bbb1169..efc357523 100644 --- a/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 +++ b/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/strings/issue1105.smt2 b/test/regress/cli/regress1/strings/issue1105.smt2 index 0a5513fec..b8ffbc503 100644 --- a/test/regress/cli/regress1/strings/issue1105.smt2 +++ b/test/regress/cli/regress1/strings/issue1105.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL) (set-option :strings-exp true) diff --git a/test/regress/cli/regress1/strings/issue6913.smt2 b/test/regress/cli/regress1/strings/issue6913.smt2 index 35626f227..c8de4349a 100644 --- a/test/regress/cli/regress1/strings/issue6913.smt2 +++ b/test/regress/cli/regress1/strings/issue6913.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ; EXPECT: unsat (set-logic ALL) (declare-fun a () String) diff --git a/test/regress/cli/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/cli/regress1/wrong-qfabvfp-smtcomp2018.smt2 index 4648c327a..176c23ec6 100644 --- a/test/regress/cli/regress1/wrong-qfabvfp-smtcomp2018.smt2 +++ b/test/regress/cli/regress1/wrong-qfabvfp-smtcomp2018.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --decision=internal -q -; COMMAND-LINE: --decision=justification -q +; COMMAND-LINE: --decision=internal +; COMMAND-LINE: --decision=justification ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_BVFP) diff --git a/test/regress/cli/regress2/bug765.smt2 b/test/regress/cli/regress2/bug765.smt2 index db87efaa1..328d81378 100644 --- a/test/regress/cli/regress2/bug765.smt2 +++ b/test/regress/cli/regress2/bug765.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --incremental --fmf-fun-rlv -q +; COMMAND-LINE: --incremental --fmf-fun-rlv +; DISABLE-TESTER: model (set-logic ALL) (declare-datatypes ((Color 0)) ( diff --git a/test/regress/cli/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/cli/regress2/quantifiers/net-policy-no-time.smt2 index b688d3fcf..e112e9b3d 100644 --- a/test/regress/cli/regress2/quantifiers/net-policy-no-time.smt2 +++ b/test/regress/cli/regress2/quantifiers/net-policy-no-time.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: sat (set-logic UFDTLIRA) (set-option :fmf-bound true) diff --git a/test/regress/cli/regress2/strings/issue6483.smt2 b/test/regress/cli/regress2/strings/issue6483.smt2 index a86ce1fe5..53a0c3ab1 100644 --- a/test/regress/cli/regress2/strings/issue6483.smt2 +++ b/test/regress/cli/regress2/strings/issue6483.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: -q ; EXPECT: unsat (set-logic QF_SLIA) (declare-fun a () String) -- 2.30.2