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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 12 Apr 2022 14:19:53 +0000 (09:19 -0500)
committer	GitHub <noreply@github.com>
	Tue, 12 Apr 2022 14:19:53 +0000 (14:19 +0000)
commit	13c3b7355c5bf0ed749f9be9b1cefb7262d08353
tree	6455b3fe040e2b2b2b16e3953085473527f08015	tree
parent	e61a7cb2c0304c28b56c569f774e3e3fedf0ce03	commit \| diff

Making some benchmarks SMT-LIB compliant for subtypes (#8600)

This makes some of our regressions compliant for arithmetic subtyping. This is required to make these benchmarks parsable when subtyping is eliminated.

We should discuss whether we should be permissive for such benchmarks. Regardless, the majority of our regressions should be SMT-LIB compliant.

77 files changed:

test/regress/cli/regress0/arith/arith-mixed-types-no-tighten.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/arith-tighten-1.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/arith.03.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/bug549.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/bug569.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/issue3683.smt2		diff \| blob \| history
test/regress/cli/regress0/arith/issue8159-rewrite-intreal.smt2		diff \| blob \| history
test/regress/cli/regress0/cores/issue3455.smt2		diff \| blob \| history
test/regress/cli/regress0/cores/issue3651.smt2		diff \| blob \| history
test/regress/cli/regress0/cores/issue5079.smt2		diff \| blob \| history
test/regress/cli/regress0/cores/issue5238.smt2		diff \| blob \| history
test/regress/cli/regress0/cvc3-bug15.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/datatypes/pair-real-bool.smt2		diff \| blob \| history
test/regress/cli/regress0/fmf/syn002-si-real-int.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/issue4277-assign-func.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/issue5734.smt2		diff \| blob \| history
test/regress/cli/regress0/fp/issue7569.smt2		diff \| blob \| history
test/regress/cli/regress0/get-value-reals-ints.smt2		diff \| blob \| history
test/regress/cli/regress0/ho/issue5744-cg-model.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/issue3475.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue7938-tf-model.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8182-exact-mv-keep.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8183-tc-pi.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/real-as-int.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/sqrt.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2		diff \| blob \| history
test/regress/cli/regress0/precedence/plus-mult.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/preprocess/preprocess_10.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/preprocess/preprocess_11.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/preprocess/preprocess_12.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/is-int.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/issue4086-infs.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/macros-real-arg.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/mix-match.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/mix-simp.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/simp-typ-test.smt2		diff \| blob \| history
test/regress/cli/regress0/smtlib/reset-assertions2.smt2		diff \| blob \| history
test/regress/cli/regress0/uflra/bug293.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/unconstrained/arith2.smt2		diff \| blob \| history
test/regress/cli/regress0/unconstrained/arith4.smt2		diff \| blob \| history
test/regress/cli/regress0/unconstrained/arith7.smt2		diff \| blob \| history
test/regress/cli/regress1/issue7937-difficulty-irr.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/issue3617.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/issue3803-nl-check-model.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/pinto-model-core-ni.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue215.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue232.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue279.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue290.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue291.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/proj-issue302.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/shifting.smt2		diff \| blob \| history
test/regress/cli/regress1/nl/shifting2.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue4412-cegqi-type.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue4685-wrewrite.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue5378-witness.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue5735-2-subtypes.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue6845-nl-lemma-tc.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue7537-cegqi-comp-types.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/mix-coeff.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3200.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3205.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3514.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3633.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3634.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue4009-qep.smt2		diff \| blob \| history

RSS Atom