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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 22 Oct 2021 20:48:25 +0000 (15:48 -0500)
committer	GitHub <noreply@github.com>
	Fri, 22 Oct 2021 20:48:25 +0000 (20:48 +0000)
commit	4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b
tree	467f72854fdc931f1d2ffc9124ab2fa841874d93	tree
parent	b3774c9758b6a23c8ef5d98eaa0879a814114674	commit \| diff

Add more abduction regressions (#7461)

Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.

30 files changed:

src/theory/builtin/theory_builtin_type_rules.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/abduct-dt.smt2	[deleted file]	blob \| history
test/regress/regress1/abduction/abd-simple-conj-4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/abduct-dt.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/abduction_streq.readable.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/issue5848-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/issue5848-4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/issue5848.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/issue6605-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/sygus-abduct-test-user.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/sygus-abduct-test.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/uf-abduct.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/yoni-true-sol.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus-abduct-ex1-grammar.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus-abduct-test-ccore.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus-abduct-test-user.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus-abduct-test.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/abd-simple-conj-4.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/abduction_streq.readable.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/uf-abduct.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/yoni-true-sol.smt2	[deleted file]	blob \| history

RSS Atom