rels « regress1 « 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--	addr_book_1.cvc.smt2	1470	log plain
-rw-r--r--	addr_book_1_1.cvc.smt2	1462	log plain
-rw-r--r--	bv1-unit.cvc.smt2	600	log plain
-rw-r--r--	bv1-unitb.cvc.smt2	649	log plain
-rw-r--r--	bv1.cvc.smt2	541	log plain
-rw-r--r--	bv1p-sat.cvc.smt2	660	log plain
-rw-r--r--	bv1p.cvc.smt2	782	log plain
-rw-r--r--	bv2.cvc.smt2	539	log plain
-rw-r--r--	garbage_collect.cvc.smt2	1735	log plain
-rw-r--r--	iden_1_1.cvc.smt2	684	log plain
-rw-r--r--	join-eq-structure-and.cvc.smt2	677	log plain
-rw-r--r--	join-eq-structure.cvc.smt2	674	log plain
-rw-r--r--	joinImg_0_1.cvc.smt2	902	log plain
-rw-r--r--	joinImg_0_2.cvc.smt2	1007	log plain
-rw-r--r--	joinImg_1.cvc.smt2	612	log plain
-rw-r--r--	joinImg_1_1.cvc.smt2	657	log plain
-rw-r--r--	joinImg_2.cvc.smt2	958	log plain
-rw-r--r--	joinImg_2_1.cvc.smt2	933	log plain
-rw-r--r--	prod-mod-eq.cvc.smt2	664	log plain
-rw-r--r--	prod-mod-eq2.cvc.smt2	737	log plain
-rw-r--r--	qgu-fuzz-relations-2.smt2	282	log plain
-rw-r--r--	qgu-fuzz-relations-3-upwards.smt2	312	log plain
-rw-r--r--	rel_complex_3.cvc.smt2	916	log plain
-rw-r--r--	rel_complex_4.cvc.smt2	1041	log plain
-rw-r--r--	rel_complex_5.cvc.smt2	1120	log plain
-rw-r--r--	rel_mix_0_1.cvc.smt2	656	log plain
-rw-r--r--	rel_pressure_0.cvc.smt2	19406	log plain
-rw-r--r--	rel_tc_10_1.cvc.smt2	459	log plain
-rw-r--r--	rel_tc_4.cvc.smt2	531	log plain
-rw-r--r--	rel_tc_4_1.cvc.smt2	281	log plain
-rw-r--r--	rel_tc_5_1.cvc.smt2	238	log plain
-rw-r--r--	rel_tc_6.cvc.smt2	249	log plain
-rw-r--r--	rel_tc_9_1.cvc.smt2	730	log plain
-rw-r--r--	rel_tp_2.cvc.smt2	340	log plain
-rw-r--r--	rel_tp_join_2_1.cvc.smt2	582	log plain
-rw-r--r--	set-strat.cvc.smt2	649	log plain
-rw-r--r--	strat.cvc.smt2	653	log plain