Description: Disable several failing test cases for now Author: Fabian Wolff Bug: https://github.com/CVC4/CVC4/issues/5082 Bug-Debian: https://bugs.debian.org/970511 Last-Update: 2020-09-17 --- This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -361,9 +361,7 @@ regress0/bv/fuzz40.smtv1.smt2 regress0/bv/fuzz41.smtv1.smt2 regress0/bv/issue3621.smt2 - regress0/bv/issue-4075.smt2 regress0/bv/issue-4076.smt2 - regress0/bv/issue-4130.smt2 regress0/bv/int_to_bv_err_on_demand_1.smt2 regress0/bv/mul-neg-unsat.smt2 regress0/bv/mul-negpow2.smt2 @@ -380,7 +378,6 @@ regress0/cvc3.userdoc.04.cvc regress0/cvc3.userdoc.05.cvc regress0/cvc3.userdoc.06.cvc - regress0/cvc-rerror-print.cvc regress0/datatypes/4482-unc-simp-one.smt2 regress0/datatypes/Test1-tup-mp.cvc regress0/datatypes/boolean-equality.cvc @@ -473,11 +470,6 @@ regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/simple-dump-model.smt2 - regress0/expect/scrub.01.smtv1.smt2 - regress0/expect/scrub.03.smt2 - regress0/expect/scrub.06.cvc - regress0/expect/scrub.08.sy - regress0/expect/scrub.09.p regress0/flet.smtv1.smt2 regress0/flet2.smtv1.smt2 regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2 @@ -544,7 +536,6 @@ regress0/ho/ho-matching-nested-app.smt2 regress0/ho/ho-std-fmf.smt2 regress0/ho/hoa0008.smt2 - regress0/ho/issue4477.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/match-middle.smt2 @@ -569,8 +560,6 @@ regress0/ite4.smt2 regress0/ite_real_int_type.smtv1.smt2 regress0/ite_real_valid.smtv1.smt2 - regress0/lang_opts_2_5.smt2 - regress0/lang_opts_2_6_1.smt2 regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2 regress0/lemmas/fs_not_sc_seen.induction.smtv1.smt2 regress0/lemmas/mode_cntrl.induction.smtv1.smt2 @@ -590,7 +579,6 @@ regress0/nl/issue3407.smt2 regress0/nl/issue3411.smt2 regress0/nl/issue3475.smt2 - regress0/nl/issue3652.smt2 regress0/nl/issue3718.smt2 regress0/nl/issue3719.smt2 regress0/nl/issue3729-cm-solved-tf.smt2 @@ -619,19 +607,13 @@ regress0/nl/subs0-unsat-confirm.smt2 regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 - regress0/options/invalid_dump.smt2 - regress0/options/invalid_option_inc_proofs.smt2 regress0/opt-abd-no-use.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 - regress0/parser/bv_nat.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 - regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 - regress0/parser/shadow_fun_symbol_all.smt2 - regress0/parser/shadow_fun_symbol_nirat.smt2 regress0/parser/strings20.smt2 regress0/parser/strings25.smt2 regress0/parser/to_fp.smt2 @@ -744,7 +726,6 @@ regress0/quantifiers/issue3655.smt2 regress0/quantifiers/issue4086-infs.smt2 regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 - regress0/quantifiers/issue4437-unc-quant.smt2 regress0/quantifiers/issue4476-ext-rew.smt2 regress0/quantifiers/issue4576.smt2 regress0/quantifiers/lra-triv-gn.smt2 @@ -868,7 +849,6 @@ regress0/sets/complement.cvc regress0/sets/complement2.cvc regress0/sets/complement3.cvc - regress0/sets/comp-qf-error.smt2 regress0/sets/cvc-sample.cvc regress0/sets/dt-simp-mem.smt2 regress0/sets/emptyset.smt2 @@ -921,21 +901,18 @@ regress0/simplification_bug2.smtv1.smt2 regress0/smallcnf.cvc regress0/smt2output.smt2 - regress0/smtlib/define-fun-rec-logic.smt2 regress0/smtlib/get-unsat-assumptions.smt2 regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 regress0/smtlib/issue4077.smt2 regress0/smtlib/issue4151.smt2 regress0/smtlib/issue4552.smt2 - regress0/smtlib/reason-unknown.smt2 regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 regress0/smtlib/reset-assertions2.smt2 regress0/smtlib/reset-assertions-global.smt2 regress0/smtlib/reset-force-logic.smt2 regress0/smtlib/reset-set-logic.smt2 - regress0/smtlib/set-info-status.smt2 regress0/strings/bidir_star.smt2 regress0/strings/bug001.smt2 regress0/strings/bug002.smt2 @@ -964,7 +941,6 @@ regress0/strings/issue4070.smt2 regress0/strings/issue4376.smt2 regress0/strings/itos-entail.smt2 - regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 regress0/strings/loop001.smt2 regress0/strings/loop-wrong-sem.smt2 @@ -1030,7 +1006,6 @@ regress0/sygus/parity-AIG-d0.sy regress0/sygus/parse-bv-let.sy regress0/sygus/pbe-pred-contra.sy - regress0/sygus/pLTL-sygus-syntax-err.sy regress0/sygus/print-define-fun.sy regress0/sygus/real-si-all.sy regress0/sygus/sygus-no-wf.sy @@ -1135,7 +1110,6 @@ regress0/uflra/simple.02.cvc regress0/uflra/simple.03.cvc regress0/uflra/simple.04.cvc - regress0/unconstrained/4481.smt2 regress0/unconstrained/arith.smt2 regress0/unconstrained/arith3.smt2 regress0/unconstrained/arith4.smt2 @@ -1222,21 +1196,16 @@ regress1/arith/arith-int-085.cvc regress1/arith/arith-int-097.cvc regress1/arith/bug547.1.smt2 - regress1/arith/bug716.0.smt2 - regress1/arith/bug716.1.cvc regress1/arith/div.03.smt2 regress1/arith/div.06.smt2 regress1/arith/div.08.smt2 - regress1/arith/div.09.smt2 regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc regress1/arith/mod.02.smt2 regress1/arith/mod.03.smt2 - regress1/arith/mult.02.smt2 regress1/arith/pbrewrites-test.smt2 regress1/arith/problem__003.smt2 - regress1/arrayinuf_error.smt2 regress1/aufbv/bug580.smt2 regress1/aufbv/fuzz10.smtv1.smt2 regress1/auflia/bug330.smt2 @@ -1245,15 +1214,12 @@ regress1/bug296.smt2 regress1/bug425.cvc regress1/bug507.smt2 - regress1/bug512.smt2 regress1/bug516.smt2 regress1/bug519.smt2 regress1/bug520.smt2 - regress1/bug521.smt2 regress1/bug543.smt2 regress1/bug567.smt2 regress1/bug593.smt2 - regress1/bug681.smt2 regress1/bug694-Unapply1.scala-0.smt2 regress1/bug800.smt2 regress1/bv/bug787.smt2 @@ -1273,12 +1239,9 @@ regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 - regress1/constarr3.cvc - regress1/constarr3.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 - regress1/datatypes/error.cvc regress1/datatypes/issue3266-small.smt2 regress1/datatypes/issue-variant-dt-zero.smt2 regress1/datatypes/manos-model.smt2 @@ -1288,8 +1251,6 @@ regress1/decision/error3.smtv1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 regress1/decision/quant-symmetric_unsat_7.smt2 - regress1/error.cvc - regress1/errorcrash.smt2 regress1/fmf-fun-dbu.smt2 regress1/fmf/ALG008-1.smt2 regress1/fmf/Hoare-z3.931718.smtv1.smt2 @@ -1323,9 +1284,7 @@ regress1/fmf/german73.smt2 regress1/fmf/issue2034-preinit.smt2 regress1/fmf/issue3587.smt2 - regress1/fmf/issue3615.smt2 regress1/fmf/issue3626.smt2 - regress1/fmf/issue3689.smt2 regress1/fmf/issue4068-si-qf.smt2 regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue916-fmf-or.smt2 @@ -1430,7 +1389,6 @@ regress1/nl/sugar-ident.smt2 regress1/nl/tan-rewrite2.smt2 regress1/nl/zero-subset.smt2 - regress1/non-fatal-errors.smt2 regress1/parsing_ringer.cvc regress1/proof00.smt2 regress1/push-pop/arith_lra_01.smt2 @@ -1512,7 +1470,6 @@ regress1/quantifiers/bignum_quant.smt2 regress1/quantifiers/bug802.smt2 regress1/quantifiers/bug822.smt2 - regress1/quantifiers/bug_743.smt2 regress1/quantifiers/burns13.smt2 regress1/quantifiers/burns4.smt2 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 @@ -1641,13 +1598,8 @@ regress1/rels/rel_tp_join_2_1.cvc regress1/rels/set-strat.cvc regress1/rels/strat.cvc - regress1/rr-verify/bool-crci.sy - regress1/rr-verify/bv-term-32.sy - regress1/rr-verify/bv-term.sy regress1/rr-verify/fp-arith.sy regress1/rr-verify/fp-bool.sy - regress1/rr-verify/regex.sy - regress1/rr-verify/string-term.sy regress1/sep/chain-int.smt2 regress1/sep/crash1220.smt2 regress1/sep/dispose-list-4-init.smt2 @@ -1692,7 +1644,6 @@ regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 - regress1/sets/arjun-set-univ.cvc regress1/sets/card-3.smt2 regress1/sets/card-4.smt2 regress1/sets/card-5.smt2 @@ -1705,7 +1656,6 @@ regress1/sets/comp-pos-member.smt2 regress1/sets/copy_check_heap_access_33_4.smt2 regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 - regress1/sets/finite-type/bug3663.smt2 regress1/sets/finite-type/sets-card-arrcolor.smt2 regress1/sets/finite-type/sets-card-arrunit.smt2 regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -1739,7 +1689,6 @@ regress1/sets/sets-tuple-poly.cvc regress1/sets/set-comp-sat.smt2 regress1/sets/sharingbug.smt2 - regress1/sets/univ-set-uf-elim.smt2 regress1/simplification_bug4.smt2 regress1/sqrt2-sort-inf-unk.smt2 regress1/strings/artemis-0512-nonterm.smt2 @@ -1854,8 +1803,6 @@ regress1/strings/type002.smt2 regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 - regress1/sygus-abduct-ex1-grammar.smt2 - regress1/sygus-abduct-test.smt2 regress1/sygus-abduct-test-ccore.smt2 regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy @@ -1871,7 +1818,6 @@ regress1/sygus/cggmp.sy regress1/sygus/clock-inc-tuple.sy regress1/sygus/coeff-solve-inv.sy - regress1/sygus/commutative-stream.sy regress1/sygus/commutative.sy regress1/sygus/concat_extract_example.sy regress1/sygus/constant-bool-si-all.sy @@ -1984,7 +1930,6 @@ regress1/sygus/tl-type-4x.sy regress1/sygus/tl-type.sy regress1/sygus/triv-type-mismatch-si.sy - regress1/sygus/trivial-stream.sy regress1/sygus/twolets1.sy regress1/sygus/twolets2-orig.sy regress1/sygus/uf-abduct.smt2 @@ -2093,7 +2038,6 @@ regress2/strings/replace_re.smt2 regress2/strings/replace_re_all.smt2 regress2/strings/replaceall-diffrange.smt2 - regress2/strings/replaceall-len-c.smt2 regress2/strings/small-1.smt2 regress2/sygus/DRAGON_1.lus.sy regress2/sygus/MPwL_d1s3.sy @@ -2155,6 +2099,62 @@ # Disabled tests, will not be run. set(regression_disabled_tests + regress1/fmf/issue3615.smt2 + regress1/fmf/issue3689.smt2 + regress2/strings/replaceall-len-c.smt2 + regress0/bv/issue-4075.smt2 + regress0/bv/issue-4130.smt2 + regress0/cvc-rerror-print.cvc + regress0/expect/scrub.01.smtv1.smt2 + regress0/expect/scrub.03.smt2 + regress0/expect/scrub.06.cvc + regress0/expect/scrub.08.sy + regress0/expect/scrub.09.p + regress0/ho/issue4477.smt2 + regress0/lang_opts_2_5.smt2 + regress0/lang_opts_2_6_1.smt2 + regress0/nl/issue3652.smt2 + regress0/options/invalid_dump.smt2 + regress0/options/invalid_option_inc_proofs.smt2 + regress0/parser/bv_nat.smt2 + regress0/parser/force_logic_set_logic.smt2 + regress0/parser/shadow_fun_symbol_all.smt2 + regress0/parser/shadow_fun_symbol_nirat.smt2 + regress0/quantifiers/issue4437-unc-quant.smt2 + regress0/sets/comp-qf-error.smt2 + regress0/smtlib/define-fun-rec-logic.smt2 + regress0/smtlib/reason-unknown.smt2 + regress0/smtlib/set-info-status.smt2 + regress0/strings/large-model.smt2 + regress0/sygus/pLTL-sygus-syntax-err.sy + regress0/unconstrained/4481.smt2 + regress1/arith/bug716.0.smt2 + regress1/arith/bug716.1.cvc + regress1/arith/div.09.smt2 + regress1/arith/mult.02.smt2 + regress1/arrayinuf_error.smt2 + regress1/bug512.smt2 + regress1/bug521.smt2 + regress1/bug681.smt2 + regress1/constarr3.cvc + regress1/constarr3.smt2 + regress1/datatypes/error.cvc + regress1/error.cvc + regress1/errorcrash.smt2 + regress1/non-fatal-errors.smt2 + regress1/quantifiers/bug_743.smt2 + regress1/rr-verify/bool-crci.sy + regress1/rr-verify/bv-term-32.sy + regress1/rr-verify/bv-term.sy + regress1/rr-verify/regex.sy + regress1/rr-verify/string-term.sy + regress1/sets/arjun-set-univ.cvc + regress1/sets/finite-type/bug3663.smt2 + regress1/sets/univ-set-uf-elim.smt2 + regress1/sygus-abduct-ex1-grammar.smt2 + regress1/sygus-abduct-test.smt2 + regress1/sygus/commutative-stream.sy + regress1/sygus/trivial-stream.sy regress3/bv_to_int_and_or.smt2 regress3/issue2429.smt2 regress3/pp-regfile.smtv1.smt2