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.smt	432	log plain
-rw-r--r--	a95test0002.smt	401	log plain
-rw-r--r--	bitvec0.delta01.smt	460	log plain
-rw-r--r--	bitvec0.smt	1790	log plain
-rw-r--r--	bitvec1.smt	1347	log plain
-rw-r--r--	bitvec2.smt	405	log plain
-rw-r--r--	bitvec3.smt	2323	log plain
-rw-r--r--	bitvec5.smt	751	log plain
-rw-r--r--	bitvec7.smt	535	log plain
-rw-r--r--	bv_eq_diamond10.smt	1311	log plain
-rw-r--r--	bv_eq_diamond11.smt	1422	log plain
-rw-r--r--	bv_eq_diamond12.smt	1538	log plain
-rw-r--r--	bv_eq_diamond13.smt	1654	log plain
-rw-r--r--	bv_eq_diamond14.smt	1770	log plain
-rw-r--r--	bv_eq_diamond15.smt	1886	log plain
-rw-r--r--	bv_eq_diamond16.smt	2002	log plain
-rw-r--r--	bv_eq_diamond17.smt	2118	log plain
-rw-r--r--	concat-merge-0.cvc	58	log plain
-rw-r--r--	concat-merge-0.smt	158	log plain
-rw-r--r--	concat-merge-1.cvc	58	log plain
-rw-r--r--	concat-merge-1.smt	158	log plain
-rw-r--r--	concat-merge-2.cvc	58	log plain
-rw-r--r--	concat-merge-2.smt	158	log plain
-rw-r--r--	concat-merge-3.cvc	58	log plain
-rw-r--r--	concat-merge-3.smt	160	log plain
-rw-r--r--	constant_core.smt2	445	log plain
-rw-r--r--	equality-00.cvc	68	log plain
-rw-r--r--	equality-00.smt	206	log plain
-rw-r--r--	equality-01.cvc	85	log plain
-rw-r--r--	equality-01.smt	258	log plain
-rw-r--r--	equality-02.cvc	212	log plain
-rw-r--r--	equality-02.smt	490	log plain
-rw-r--r--	equality-03.cvc	274	log plain
-rw-r--r--	equality-03.smt	681	log plain
-rw-r--r--	equality-04.smt	1091	log plain
-rw-r--r--	equality-05.cvc	82	log plain
-rw-r--r--	equality-05.smt	203	log plain
-rw-r--r--	ext_con_004_001_1024.smt	1167	log plain
-rw-r--r--	extract-concat-0.cvc	56	log plain
-rw-r--r--	extract-concat-0.smt	176	log plain
-rw-r--r--	extract-concat-1.cvc	56	log plain
-rw-r--r--	extract-concat-1.smt	176	log plain
-rw-r--r--	extract-concat-10.cvc	65	log plain
-rw-r--r--	extract-concat-10.smt	202	log plain
-rw-r--r--	extract-concat-11.cvc	65	log plain
-rw-r--r--	extract-concat-11.smt	202	log plain
-rw-r--r--	extract-concat-2.cvc	56	log plain
-rw-r--r--	extract-concat-2.smt	176	log plain
-rw-r--r--	extract-concat-3.cvc	56	log plain
-rw-r--r--	extract-concat-3.smt	176	log plain
-rw-r--r--	extract-concat-4.cvc	55	log plain
-rw-r--r--	extract-concat-4.smt	175	log plain
-rw-r--r--	extract-concat-5.cvc	55	log plain
-rw-r--r--	extract-concat-5.smt	175	log plain
-rw-r--r--	extract-concat-6.cvc	55	log plain
-rw-r--r--	extract-concat-6.smt	175	log plain
-rw-r--r--	extract-concat-7.cvc	55	log plain
-rw-r--r--	extract-concat-7.smt	175	log plain
-rw-r--r--	extract-concat-8.cvc	65	log plain
-rw-r--r--	extract-concat-8.smt	202	log plain
-rw-r--r--	extract-concat-9.cvc	65	log plain
-rw-r--r--	extract-concat-9.smt	202	log plain
-rw-r--r--	extract-constant.cvc	41	log plain
-rw-r--r--	extract-constant.smt	99	log plain
-rw-r--r--	extract-extract-0.cvc	52	log plain
-rw-r--r--	extract-extract-0.smt	161	log plain
-rw-r--r--	extract-extract-1.cvc	52	log plain
-rw-r--r--	extract-extract-1.smt	150	log plain
-rw-r--r--	extract-extract-10.cvc	49	log plain
-rw-r--r--	extract-extract-10.smt	147	log plain
-rw-r--r--	extract-extract-11.cvc	86	log plain
-rw-r--r--	extract-extract-11.smt	245	log plain
-rw-r--r--	extract-extract-2.cvc	51	log plain
-rw-r--r--	extract-extract-2.smt	148	log plain
-rw-r--r--	extract-extract-3.cvc	51	log plain
-rw-r--r--	extract-extract-3.smt	148	log plain
-rw-r--r--	extract-extract-4.cvc	52	log plain
-rw-r--r--	extract-extract-4.smt	161	log plain
-rw-r--r--	extract-extract-5.cvc	51	log plain
-rw-r--r--	extract-extract-5.smt	148	log plain
-rw-r--r--	extract-extract-6.cvc	51	log plain
-rw-r--r--	extract-extract-6.smt	148	log plain
-rw-r--r--	extract-extract-7.cvc	51	log plain
-rw-r--r--	extract-extract-7.smt	148	log plain
-rw-r--r--	extract-extract-8.cvc	49	log plain
-rw-r--r--	extract-extract-8.smt	159	log plain
-rw-r--r--	extract-extract-9.cvc	49	log plain
-rw-r--r--	extract-extract-9.smt	147	log plain
-rw-r--r--	extract-whole-0.cvc	113	log plain
-rw-r--r--	extract-whole-0.smt	291	log plain
-rw-r--r--	extract-whole-1.cvc	81	log plain
-rw-r--r--	extract-whole-1.smt	227	log plain
-rw-r--r--	extract-whole-2.cvc	96	log plain
-rw-r--r--	extract-whole-2.smt	215	log plain
-rw-r--r--	extract-whole-3.cvc	95	log plain
-rw-r--r--	extract-whole-3.smt	215	log plain
-rw-r--r--	extract-whole-4.cvc	41	log plain
-rw-r--r--	extract-whole-4.smt	118	log plain
-rw-r--r--	incremental.smt	617	log plain
-rw-r--r--	slice-01.cvc	82	log plain
-rw-r--r--	slice-01.smt	215	log plain
-rw-r--r--	slice-02.cvc	81	log plain
-rw-r--r--	slice-02.smt	214	log plain
-rw-r--r--	slice-03.cvc	128	log plain
-rw-r--r--	slice-03.smt	312	log plain
-rw-r--r--	slice-04.cvc	284	log plain
-rw-r--r--	slice-04.smt	521	log plain
-rw-r--r--	slice-05.cvc	286	log plain
-rw-r--r--	slice-05.smt	523	log plain
-rw-r--r--	slice-06.cvc	291	log plain
-rw-r--r--	slice-06.smt	538	log plain
-rw-r--r--	slice-07.cvc	66	log plain
-rw-r--r--	slice-07.smt	186	log plain
-rw-r--r--	slice-08.cvc	66	log plain
-rw-r--r--	slice-08.smt	184	log plain
-rw-r--r--	slice-09.cvc	66	log plain
-rw-r--r--	slice-09.smt	186	log plain
-rw-r--r--	slice-10.cvc	98	log plain
-rw-r--r--	slice-10.smt	196	log plain
-rw-r--r--	slice-11.cvc	92	log plain
-rw-r--r--	slice-11.smt	231	log plain
-rw-r--r--	slice-12.cvc	195	log plain
-rw-r--r--	slice-12.smt	484	log plain
-rw-r--r--	slice-13.cvc	195	log plain
-rw-r--r--	slice-13.smt	484	log plain
-rw-r--r--	slice-14.cvc	103	log plain
-rw-r--r--	slice-14.smt	203	log plain
-rw-r--r--	slice-15.cvc	105	log plain
-rw-r--r--	slice-15.smt	213	log plain
-rw-r--r--	slice-16.cvc	105	log plain
-rw-r--r--	slice-16.smt	213	log plain
-rw-r--r--	slice-17.cvc	161	log plain
-rw-r--r--	slice-17.smt	315	log plain
-rw-r--r--	slice-18.cvc	161	log plain
-rw-r--r--	slice-18.smt	315	log plain
-rw-r--r--	slice-19.cvc	162	log plain
-rw-r--r--	slice-19.smt	315	log plain
-rw-r--r--	slice-20.cvc	190	log plain
-rw-r--r--	slice-20.smt	425	log plain