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--	NEQ016_size5_reduced2a.smtv1.smt2	253	log plain
-rw-r--r--	NEQ016_size5_reduced2b.smtv1.smt2	253	log plain
-rw-r--r--	PEQ018_size4.smtv1.smt2	6219	log plain
-rw-r--r--	SEQ032_size2.smtv1.smt2	1864	log plain
-rw-r--r--	bool-pred-nested.smt2	141	log plain
-rw-r--r--	ccredesign-fuzz.smtv1.smt2	583	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.smtv1.smt2	19680	log plain
-rw-r--r--	eq_diamond1.smtv1.smt2	449	log plain
-rw-r--r--	eq_diamond14.reduced.smtv1.smt2	1305	log plain
-rw-r--r--	eq_diamond14.reduced2.smtv1.smt2	1400	log plain
-rw-r--r--	eq_diamond23.smtv1.smt2	3299	log plain
-rw-r--r--	euf_simp01.smtv1.smt2	374	log plain
-rw-r--r--	euf_simp02.smtv1.smt2	569	log plain
-rw-r--r--	euf_simp03.smtv1.smt2	484	log plain
-rw-r--r--	euf_simp04.smtv1.smt2	543	log plain
-rw-r--r--	euf_simp05.smtv1.smt2	356	log plain
-rw-r--r--	euf_simp06.smtv1.smt2	364	log plain
-rw-r--r--	euf_simp08.smtv1.smt2	369	log plain
-rw-r--r--	euf_simp09.smtv1.smt2	368	log plain
-rw-r--r--	euf_simp10.smtv1.smt2	392	log plain
-rw-r--r--	euf_simp11.smtv1.smt2	407	log plain
-rw-r--r--	euf_simp12.smtv1.smt2	411	log plain
-rw-r--r--	euf_simp13.smtv1.smt2	567	log plain
-rw-r--r--	iso_brn001.smtv1.smt2	17170	log plain
-rw-r--r--	iso_icl_repgen004.smtv1.smt2	53198	log plain
-rw-r--r--	issue2947.smt2	163	log plain
-rw-r--r--	mkpidgeon	760	log plain
-rw-r--r--	pred.smtv1.smt2	307	log plain
-rw-r--r--	simple.01.cvc	88	log plain
-rw-r--r--	simple.02.cvc	83	log plain
-rw-r--r--	simple.03.cvc	137	log plain
-rw-r--r--	simple.04.cvc	140	log plain