projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 533f87d) | patch
[Regressions] Do not test `--check-proofs` anymore (#4914)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 19 Aug 2020 14:08:22 +0000 (07:08 -0700)
committerGitHub <noreply@github.com>
Wed, 19 Aug 2020 14:08:22 +0000 (09:08 -0500)
commit41f1a9a0036f3d18ec21ef6005fb218cf704fe60
treecc314d03286ff6bbd15c157ae06d7bc436d8f831tree
parent533f87dc6cf44a7bcb84694a5c21e5280425be93commit | diff
[Regressions] Do not test `--check-proofs` anymore (#4914)

In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.
53 files changed:
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/ite-lift.smt2 diff | blob | history
test/regress/regress0/arrays/incorrect10.smtv1.smt2 diff | blob | history
test/regress/regress0/bv/ackermann2.smt2 diff | blob | history
test/regress/regress0/bv/ackermann3.smt2 diff | blob | history
test/regress/regress0/bv/ackermann4.smt2 diff | blob | history
test/regress/regress0/bv/ackermann5.smt2 diff | blob | history
test/regress/regress0/bv/ackermann6.smt2 diff | blob | history
test/regress/regress0/bv/ackermann7.smt2 diff | blob | history
test/regress/regress0/bv/ackermann8.smt2 diff | blob | history
test/regress/regress0/bv/bv-int-collapse1.smt2 diff | blob | history
test/regress/regress0/bv/bv-int-collapse2.smt2 diff | blob | history
test/regress/regress0/bv/bv-options1.smt2 [deleted file] blob | history
test/regress/regress0/bv/bv-options2.smt2 [deleted file] blob | history
test/regress/regress0/bv/bv-options3.smt2 [deleted file] blob | history
test/regress/regress0/bv/bv-options4.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bitwise.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvmul2.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_zext.smt2 diff | blob | history
test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 diff | blob | history
test/regress/regress0/bv/core/slice-12.smtv1.smt2 diff | blob | history
test/regress/regress0/bv/test-bv_intro_pow2.smt2 diff | blob | history
test/regress/regress0/datatypes/empty_tuprec.cvc diff | blob | history
test/regress/regress0/fmf/sort-infer-typed-082718.smt2 diff | blob | history
test/regress/regress0/get-value-ints.smt2 diff | blob | history
test/regress/regress0/get-value-reals-ints.smt2 diff | blob | history
test/regress/regress0/get-value-reals.smt2 diff | blob | history
test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 diff | blob | history
test/regress/regress0/printer/bv_consts_bin.smt2 diff | blob | history
test/regress/regress0/proof_no_support.smt2 [deleted file] blob | history
test/regress/regress0/quantifiers/lra-triv-gn.smt2 diff | blob | history
test/regress/regress0/uflra/constants0.smtv1.smt2 diff | blob | history
test/regress/regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2 diff | blob | history
test/regress/regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2 diff | blob | history
test/regress/regress1/bv/bv2nat-ground.smt2 diff | blob | history
test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 diff | blob | history
test/regress/regress1/fmf/PUZ001+1.smt2 diff | blob | history
test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 diff | blob | history
test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 diff | blob | history
test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 diff | blob | history
test/regress/regress1/nl/nl_uf_lalt.smt2 diff | blob | history
test/regress/regress1/quantifiers/qe-partial.smt2 diff | blob | history
test/regress/regress1/quantifiers/qe.smt2 diff | blob | history
test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 diff | blob | history
test/regress/regress2/arith/pursuit-safety-11.smtv1.smt2 diff | blob | history
test/regress/regress2/arith/pursuit-safety-12.smtv1.smt2 diff | blob | history
test/regress/regress2/bv_to_int_ashr.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_1.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_2.smt2 diff | blob | history
test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p diff | blob | history
test/regress/regress3/bv_to_int_and_or.smt2 diff | blob | history
test/regress/run_regression.py diff | blob | history