git.libre-soc.org Git - cvc5.git/commit

author	Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
	Thu, 21 Apr 2022 06:45:04 +0000 (01:45 -0500)
committer	GitHub <noreply@github.com>
	Thu, 21 Apr 2022 06:45:04 +0000 (06:45 +0000)
commit	017507462863ff79583df3ce5eb2b24ad0c75611
tree	ceaf238799cac0249cdf358ce859d5adb1612650	tree
parent	76465f3dbe7d9a54ef4ea6c10997b4f0996590fa	commit \| diff

Add tester for LFSC printer. (#8606)

This adds an option to check the LFSC proofs generated by `cvc5` for unsat benchmarks. This does not enable the tester in CI as it fails for many benchmarks.

41 files changed:

test/regress/cli/CMakeLists.txt		diff \| blob \| history
test/regress/cli/regress0/bv/div_mod.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/bv/fuzz15.delta01.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress0/bv/fuzz38.delta01.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/issue-5524.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/rti_3_5_bug.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/word-blast.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2		diff \| blob \| history
test/regress/cli/regress0/seq/seq-types.smt2		diff \| blob \| history
test/regress/cli/regress1/aufbv/bug348.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress1/auflia/bug330.smt2		diff \| blob \| history
test/regress/cli/regress1/bv/divtest.smt2		diff \| blob \| history
test/regress/cli/regress1/bv/fuzz38.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress1/bv/incorrect1.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2		diff \| blob \| history
test/regress/cli/regress1/bvdiv2.smt2		diff \| blob \| history
test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2		diff \| blob \| history
test/regress/cli/regress1/issue3970-nl-ext-purify.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/NUM878.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/qbv-test-invert-bvcomp.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/comp-intersect.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/comp-odd.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/comp-pos-member.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/comp-positive.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3201.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3247.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue4009-qep.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/proj-issue185.smt2		diff \| blob \| history
test/regress/cli/regress2/bug349.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress2/fp/issue7056.smt2		diff \| blob \| history
test/regress/cli/regress2/instance_1444.smtv1.smt2		diff \| blob \| history
test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2		diff \| blob \| history
test/regress/cli/regress2/ooo.tag10.smt2		diff \| blob \| history
test/regress/cli/run_regression.py		diff \| blob \| history

RSS Atom