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

Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.

15 files changed:

src/theory/theoryof_table_middle.h		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
test/regress/regress0/uf/Makefile.am		diff \| blob \| history
test/regress/regress0/uf/euf_simp01.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp02.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp03.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp04.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp05.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp06.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp08.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp09.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp10.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp11.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp12.smt	[new file with mode: 0644]	blob
test/regress/regress0/uf/euf_simp13.smt	[new file with mode: 0644]	blob