regress2 « 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--	DTP_k2_n35_c175_s15.smt2	10319	log plain
-rw-r--r--	FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2	50807	log plain
-rw-r--r--	GEO123+1.minimized.smt2	63175	log plain
d---------	arith	360	log plain
-rw-r--r--	bug136.smtv1.smt2	442617	log plain
-rw-r--r--	bug148.smtv1.smt2	9822	log plain
-rw-r--r--	bug349.smtv1.smt2	2729	log plain
-rw-r--r--	bug374.smtv1.smt2	1072224	log plain
-rw-r--r--	bug394.smt2	78768	log plain
-rw-r--r--	bug674.smt2	1055	log plain
-rw-r--r--	bug765.smt2	871	log plain
-rw-r--r--	bug812.smt2	31804	log plain
d---------	bv	64	log plain
-rw-r--r--	bv_to_int2.smt2	219	log plain
-rw-r--r--	bv_to_int_5095.smt2	246	log plain
-rw-r--r--	bv_to_int_5095_2.smt2	200	log plain
-rw-r--r--	bv_to_int_ashr.smt2	222	log plain
-rw-r--r--	bv_to_int_bitwise.smt2	465	log plain
-rw-r--r--	bv_to_int_bvmul1.smt2	248	log plain
-rw-r--r--	bv_to_int_bvuf_to_intuf_smtlib.smt2	2952	log plain
-rw-r--r--	bv_to_int_inc1.smt2	572	log plain
-rw-r--r--	bv_to_int_mask_array_1.smt2	485	log plain
-rw-r--r--	bv_to_int_mask_array_2.smt2	466	log plain
-rw-r--r--	bv_to_int_mask_array_3.smt2	273	log plain
-rw-r--r--	bv_to_int_shifts.smt2	554	log plain
-rw-r--r--	error1.smtv1.smt2	25011	log plain
-rw-r--r--	fuzz_2.smtv1.smt2	25586	log plain
-rw-r--r--	hash_sat_06_19.smt2	24689	log plain
-rw-r--r--	hash_sat_07_17.smt2	29767	log plain
-rw-r--r--	hash_sat_09_09.smt2	25980	log plain
-rw-r--r--	hash_sat_10_09.smt2	31951	log plain
d---------	ho	250	log plain
-rw-r--r--	hole7.cvc	7021	log plain
-rw-r--r--	hole8.cvc	10069	log plain
-rw-r--r--	instance_1444.smtv1.smt2	163009	log plain
-rw-r--r--	issue3687-check-models.smt2	2665	log plain
-rw-r--r--	issue4707-bv-to-bool-large.smt2	6831	log plain
-rw-r--r--	issue6495-dup-pat-term.smt2	20778	log plain
-rw-r--r--	javafe.ast.StandardPrettyPrint.319_no_forall.smt2	116426	log plain
-rw-r--r--	javafe.ast.WhileStmt.447_no_forall.smt2	83179	log plain
d---------	lemmas	74	log plain
d---------	nl	151	log plain
-rw-r--r--	ooo.rf6.smt2	10010	log plain
-rw-r--r--	ooo.tag10.smt2	43786	log plain
-rw-r--r--	piVC_5581bd.smt2	3987	log plain
d---------	push-pop	71	log plain
d---------	quantifiers	628	log plain
-rw-r--r--	simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2	84910	log plain
d---------	strings	938	log plain
d---------	sygus	896	log plain
-rw-r--r--	typed_v1l50016-simp.cvc	2274	log plain
-rw-r--r--	uflia-error0.smt2	360988	log plain
-rw-r--r--	xs-09-16-3-4-1-5.smtv1.smt2	6601	log plain