projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5421d1a) | patch
Remove instances of `check-proofs` in regressions. (#8630)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Mon, 18 Apr 2022 22:21:22 +0000 (17:21 -0500)
committerGitHub <noreply@github.com>
Mon, 18 Apr 2022 22:21:22 +0000 (22:21 +0000)
commit427d38c14eb23026e6866ad4b2663e3d6e82399e
treeabd25ec73b322a28e72f6b2acf204ade7a73482etree
parent5421d1a6f3035ca76feba80dca456a09633c7230commit | diff
Remove instances of `check-proofs` in regressions. (#8630)

This PR removes usages of check-proofs option according to the following rules:

unsat and no-check-proofs --> DISABLE-TESTER: proof
unsat and check-proofs --> remove option
sat and no-check-proofs --> remove option
sat and check-proofs --> change to produce-proofs
no-produce-proofs --> DISABLE-TESTER: proof
20 files changed:
test/regress/cli/regress0/arith/issue5219-conflict-rewrite.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 diff | blob | history
test/regress/cli/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 diff | blob | history
test/regress/cli/regress0/proofs/proj-issue326-nl-bounds-check.smt2 diff | blob | history
test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 diff | blob | history
test/regress/cli/regress0/proofs/project-issue330-eqproof.smt2 diff | blob | history
test/regress/cli/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 diff | blob | history
test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 diff | blob | history
test/regress/cli/regress1/hole6.cvc.smt2 diff | blob | history
test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 diff | blob | history
test/regress/cli/regress1/nl/factor_agg_s.smt2 diff | blob | history
test/regress/cli/regress1/sets/sets-disequal.smt2 diff | blob | history
test/regress/cli/regress1/strings/proj-issue331.smt2 diff | blob | history
test/regress/cli/regress2/instance_1444.smtv1.smt2 diff | blob | history
test/regress/cli/run_regression.py diff | blob | history