core « bv « 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--	a78test0002.smtv1.smt2	483	log plain
-rw-r--r--	a95test0002.smtv1.smt2	454	log plain
-rw-r--r--	bitvec0.delta01.smtv1.smt2	290	log plain
-rw-r--r--	bitvec0.smtv1.smt2	1952	log plain
-rw-r--r--	bitvec1.smtv1.smt2	1432	log plain
-rw-r--r--	bitvec2.smtv1.smt2	477	log plain
-rw-r--r--	bitvec3.smtv1.smt2	2538	log plain
-rw-r--r--	bitvec5.smtv1.smt2	845	log plain
-rw-r--r--	bitvec7.smtv1.smt2	628	log plain
-rw-r--r--	bv_eq_diamond10.smtv1.smt2	1903	log plain
-rw-r--r--	bv_eq_diamond11.smtv1.smt2	2068	log plain
-rw-r--r--	bv_eq_diamond12.smtv1.smt2	2238	log plain
-rw-r--r--	bv_eq_diamond13.smtv1.smt2	2408	log plain
-rw-r--r--	bv_eq_diamond14.smtv1.smt2	2578	log plain
-rw-r--r--	bv_eq_diamond15.smtv1.smt2	2748	log plain
-rw-r--r--	bv_eq_diamond16.smtv1.smt2	2918	log plain
-rw-r--r--	bv_eq_diamond17.smtv1.smt2	3088	log plain
-rw-r--r--	concat-merge-0.cvc	58	log plain
-rw-r--r--	concat-merge-0.smtv1.smt2	212	log plain
-rw-r--r--	concat-merge-1.cvc	58	log plain
-rw-r--r--	concat-merge-1.smtv1.smt2	212	log plain
-rw-r--r--	concat-merge-2.cvc	58	log plain
-rw-r--r--	concat-merge-2.smtv1.smt2	212	log plain
-rw-r--r--	concat-merge-3.cvc	58	log plain
-rw-r--r--	concat-merge-3.smtv1.smt2	214	log plain
-rw-r--r--	constant_core.smt2	446	log plain
-rw-r--r--	equality-00.cvc	68	log plain
-rw-r--r--	equality-00.smtv1.smt2	247	log plain
-rw-r--r--	equality-01.cvc	85	log plain
-rw-r--r--	equality-01.smtv1.smt2	297	log plain
-rw-r--r--	equality-02.cvc	212	log plain
-rw-r--r--	equality-02.smtv1.smt2	521	log plain
-rw-r--r--	equality-03.cvc	274	log plain
-rw-r--r--	equality-03.smtv1.smt2	759	log plain
-rw-r--r--	equality-04.smtv1.smt2	1655	log plain
-rw-r--r--	equality-05.cvc	82	log plain
-rw-r--r--	equality-05.smtv1.smt2	236	log plain
-rw-r--r--	ext_con_004_001_1024.smtv1.smt2	1162	log plain
-rw-r--r--	extract-concat-0.cvc	56	log plain
-rw-r--r--	extract-concat-0.smtv1.smt2	230	log plain
-rw-r--r--	extract-concat-1.cvc	56	log plain
-rw-r--r--	extract-concat-1.smtv1.smt2	230	log plain
-rw-r--r--	extract-concat-10.cvc	65	log plain
-rw-r--r--	extract-concat-10.smtv1.smt2	259	log plain
-rw-r--r--	extract-concat-11.cvc	65	log plain
-rw-r--r--	extract-concat-11.smtv1.smt2	259	log plain
-rw-r--r--	extract-concat-2.cvc	56	log plain
-rw-r--r--	extract-concat-2.smtv1.smt2	230	log plain
-rw-r--r--	extract-concat-3.cvc	56	log plain
-rw-r--r--	extract-concat-3.smtv1.smt2	230	log plain
-rw-r--r--	extract-concat-4.cvc	55	log plain
-rw-r--r--	extract-concat-4.smtv1.smt2	229	log plain
-rw-r--r--	extract-concat-5.cvc	55	log plain
-rw-r--r--	extract-concat-5.smtv1.smt2	229	log plain
-rw-r--r--	extract-concat-6.cvc	55	log plain
-rw-r--r--	extract-concat-6.smtv1.smt2	229	log plain
-rw-r--r--	extract-concat-7.cvc	55	log plain
-rw-r--r--	extract-concat-7.smtv1.smt2	229	log plain
-rw-r--r--	extract-concat-8.cvc	65	log plain
-rw-r--r--	extract-concat-8.smtv1.smt2	259	log plain
-rw-r--r--	extract-concat-9.cvc	65	log plain
-rw-r--r--	extract-concat-9.smtv1.smt2	259	log plain
-rw-r--r--	extract-constant.cvc	41	log plain
-rw-r--r--	extract-constant.smtv1.smt2	150	log plain
-rw-r--r--	extract-extract-0.cvc	52	log plain
-rw-r--r--	extract-extract-0.smtv1.smt2	214	log plain
-rw-r--r--	extract-extract-1.cvc	52	log plain
-rw-r--r--	extract-extract-1.smtv1.smt2	204	log plain
-rw-r--r--	extract-extract-10.cvc	49	log plain
-rw-r--r--	extract-extract-10.smtv1.smt2	201	log plain
-rw-r--r--	extract-extract-11.cvc	86	log plain
-rw-r--r--	extract-extract-11.smtv1.smt2	317	log plain
-rw-r--r--	extract-extract-2.cvc	51	log plain
-rw-r--r--	extract-extract-2.smtv1.smt2	202	log plain
-rw-r--r--	extract-extract-3.cvc	51	log plain
-rw-r--r--	extract-extract-3.smtv1.smt2	202	log plain
-rw-r--r--	extract-extract-4.cvc	52	log plain
-rw-r--r--	extract-extract-4.smtv1.smt2	214	log plain
-rw-r--r--	extract-extract-5.cvc	51	log plain
-rw-r--r--	extract-extract-5.smtv1.smt2	202	log plain
-rw-r--r--	extract-extract-6.cvc	51	log plain
-rw-r--r--	extract-extract-6.smtv1.smt2	202	log plain
-rw-r--r--	extract-extract-7.cvc	51	log plain
-rw-r--r--	extract-extract-7.smtv1.smt2	202	log plain
-rw-r--r--	extract-extract-8.cvc	49	log plain
-rw-r--r--	extract-extract-8.smtv1.smt2	212	log plain
-rw-r--r--	extract-extract-9.cvc	49	log plain
-rw-r--r--	extract-extract-9.smtv1.smt2	201	log plain
-rw-r--r--	extract-whole-0.cvc	113	log plain
-rw-r--r--	extract-whole-0.smtv1.smt2	363	log plain
-rw-r--r--	extract-whole-1.cvc	81	log plain
-rw-r--r--	extract-whole-1.smtv1.smt2	287	log plain
-rw-r--r--	extract-whole-2.cvc	96	log plain
-rw-r--r--	extract-whole-2.smtv1.smt2	281	log plain
-rw-r--r--	extract-whole-3.cvc	95	log plain
-rw-r--r--	extract-whole-3.smtv1.smt2	281	log plain
-rw-r--r--	extract-whole-4.cvc	41	log plain
-rw-r--r--	extract-whole-4.smtv1.smt2	166	log plain
-rw-r--r--	incremental.smtv1.smt2	419	log plain
-rw-r--r--	slice-01.cvc	82	log plain
-rw-r--r--	slice-01.smtv1.smt2	261	log plain
-rw-r--r--	slice-02.cvc	81	log plain
-rw-r--r--	slice-02.smtv1.smt2	260	log plain
-rw-r--r--	slice-03.cvc	128	log plain
-rw-r--r--	slice-03.smtv1.smt2	354	log plain
-rw-r--r--	slice-04.cvc	284	log plain
-rw-r--r--	slice-04.smtv1.smt2	554	log plain
-rw-r--r--	slice-05.cvc	286	log plain
-rw-r--r--	slice-05.smtv1.smt2	556	log plain
-rw-r--r--	slice-06.cvc	291	log plain
-rw-r--r--	slice-06.smtv1.smt2	574	log plain
-rw-r--r--	slice-07.cvc	66	log plain
-rw-r--r--	slice-07.smtv1.smt2	235	log plain
-rw-r--r--	slice-08.cvc	66	log plain
-rw-r--r--	slice-08.smtv1.smt2	233	log plain
-rw-r--r--	slice-09.cvc	66	log plain
-rw-r--r--	slice-09.smtv1.smt2	235	log plain
-rw-r--r--	slice-10.cvc	98	log plain
-rw-r--r--	slice-10.smtv1.smt2	243	log plain
-rw-r--r--	slice-11.cvc	92	log plain
-rw-r--r--	slice-11.smtv1.smt2	286	log plain
-rw-r--r--	slice-12.cvc	195	log plain
-rw-r--r--	slice-12.smtv1.smt2	977	log plain
-rw-r--r--	slice-13.cvc	195	log plain
-rw-r--r--	slice-13.smtv1.smt2	545	log plain
-rw-r--r--	slice-14.cvc	103	log plain
-rw-r--r--	slice-14.smtv1.smt2	250	log plain
-rw-r--r--	slice-15.cvc	105	log plain
-rw-r--r--	slice-15.smtv1.smt2	260	log plain
-rw-r--r--	slice-16.cvc	105	log plain
-rw-r--r--	slice-16.smtv1.smt2	258	log plain
-rw-r--r--	slice-17.cvc	161	log plain
-rw-r--r--	slice-17.smtv1.smt2	361	log plain
-rw-r--r--	slice-18.cvc	161	log plain
-rw-r--r--	slice-18.smtv1.smt2	361	log plain
-rw-r--r--	slice-19.cvc	162	log plain
-rw-r--r--	slice-19.smtv1.smt2	361	log plain
-rw-r--r--	slice-20.cvc	190	log plain
-rw-r--r--	slice-20.smtv1.smt2	457	log plain