uf « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	Makefile	139	log plain
-rw-r--r--	Makefile.am	1024	log plain
-rw-r--r--	NEQ016_size5_reduced2a.smt	190	log plain
-rw-r--r--	NEQ016_size5_reduced2b.smt	190	log plain
-rw-r--r--	PEQ018_size4.smt	6275	log plain
-rw-r--r--	SEQ032_size2.smt	1534	log plain
-rw-r--r--	bug217.smt2	329	log plain
-rw-r--r--	dead_dnd002.smt	20139	log plain
-rw-r--r--	eq_diamond1.smt	338	log plain
-rw-r--r--	eq_diamond14.reduced.smt	2118	log plain
-rw-r--r--	eq_diamond14.reduced2.smt	2454	log plain
-rw-r--r--	eq_diamond23.smt	2193	log plain
-rw-r--r--	euf_simp01.smt	308	log plain
-rw-r--r--	euf_simp02.smt	394	log plain
-rw-r--r--	euf_simp03.smt	360	log plain
-rw-r--r--	euf_simp04.smt	413	log plain
-rw-r--r--	euf_simp05.smt	294	log plain
-rw-r--r--	euf_simp06.smt	302	log plain
-rw-r--r--	euf_simp08.smt	309	log plain
-rw-r--r--	euf_simp09.smt	306	log plain
-rw-r--r--	euf_simp10.smt	331	log plain
-rw-r--r--	euf_simp11.smt	350	log plain
-rw-r--r--	euf_simp12.smt	388	log plain
-rw-r--r--	euf_simp13.smt	520	log plain
-rw-r--r--	iso_brn001.smt	17556	log plain
-rw-r--r--	iso_icl_repgen004.smt	48303	log plain
-rw-r--r--	pred.smt	191	log plain
-rw-r--r--	simple.01.cvc	96	log plain
-rw-r--r--	simple.02.cvc	89	log plain
-rw-r--r--	simple.03.cvc	145	log plain
-rw-r--r--	simple.04.cvc	146	log plain