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	1568	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--	bool-pred-nested.smt2	141	log plain
-rw-r--r--	ccredesign-fuzz.smt	731	log plain
-rw-r--r--	cnf-and-neg.smt2	270	log plain
-rw-r--r--	cnf-iff-base.smt2	321	log plain
-rw-r--r--	cnf-iff.smt2	909	log plain
-rw-r--r--	cnf-ite.smt2	838	log plain
-rw-r--r--	cnf_abc.smt2	1932	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--	gensys_brn001.smt2	37318	log plain
-rw-r--r--	iso_brn001.smt	17556	log plain
-rw-r--r--	iso_icl_repgen004.smt	48303	log plain
-rw-r--r--	mkpidgeon	760	log plain
-rw-r--r--	pred.smt	191	log plain
-rw-r--r--	proof00.smt2	1911	log plain
-rw-r--r--	simple.01.cvc	85	log plain
-rw-r--r--	simple.02.cvc	78	log plain
-rw-r--r--	simple.03.cvc	134	log plain
-rw-r--r--	simple.04.cvc	135	log plain