arith « 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--	arith-brab-test.smt2	406	log plain
-rw-r--r--	arith-int-001.cvc	741	log plain
-rw-r--r--	arith-int-002.cvc	743	log plain
-rw-r--r--	arith-int-003.cvc	746	log plain
-rw-r--r--	arith-int-004.cvc	739	log plain
-rw-r--r--	arith-int-005.cvc	740	log plain
-rw-r--r--	arith-int-006.cvc	479	log plain
-rw-r--r--	arith-int-007.cvc	494	log plain
-rw-r--r--	arith-int-008.cvc	495	log plain
-rw-r--r--	arith-int-009.cvc	492	log plain
-rw-r--r--	arith-int-010.cvc	482	log plain
-rw-r--r--	arith-int-011.cvc	177	log plain
-rw-r--r--	arith-int-012.cvc	182	log plain
-rw-r--r--	arith-int-013.cvc	180	log plain
-rw-r--r--	arith-int-016.cvc	1108	log plain
-rw-r--r--	arith-int-017.cvc	1108	log plain
-rw-r--r--	arith-int-018.cvc	1123	log plain
-rw-r--r--	arith-int-019.cvc	1109	log plain
-rw-r--r--	arith-int-020.cvc	1106	log plain
-rw-r--r--	arith-int-022.cvc	119	log plain
-rw-r--r--	arith-int-024.cvc	116	log plain
-rw-r--r--	arith-int-026.cvc	1174	log plain
-rw-r--r--	arith-int-027.cvc	1178	log plain
-rw-r--r--	arith-int-028.cvc	1176	log plain
-rw-r--r--	arith-int-029.cvc	1181	log plain
-rw-r--r--	arith-int-030.cvc	1175	log plain
-rw-r--r--	arith-int-031.cvc	1064	log plain
-rw-r--r--	arith-int-032.cvc	1052	log plain
-rw-r--r--	arith-int-033.cvc	1046	log plain
-rw-r--r--	arith-int-034.cvc	1052	log plain
-rw-r--r--	arith-int-035.cvc	1045	log plain
-rw-r--r--	arith-int-036.cvc	865	log plain
-rw-r--r--	arith-int-037.cvc	872	log plain
-rw-r--r--	arith-int-038.cvc	859	log plain
-rw-r--r--	arith-int-039.cvc	862	log plain
-rw-r--r--	arith-int-040.cvc	869	log plain
-rw-r--r--	arith-int-041.cvc	432	log plain
-rw-r--r--	arith-int-043.cvc	429	log plain
-rw-r--r--	arith-int-044.cvc	466	log plain
-rw-r--r--	arith-int-045.cvc	422	log plain
-rw-r--r--	arith-int-046.cvc	243	log plain
-rw-r--r--	arith-int-047.cvc	244	log plain
-rw-r--r--	arith-int-048.cvc	242	log plain
-rw-r--r--	arith-int-049.cvc	247	log plain
-rw-r--r--	arith-int-050.cvc	242	log plain
-rw-r--r--	arith-int-051.cvc	614	log plain
-rw-r--r--	arith-int-052.cvc	613	log plain
-rw-r--r--	arith-int-053.cvc	605	log plain
-rw-r--r--	arith-int-054.cvc	613	log plain
-rw-r--r--	arith-int-055.cvc	615	log plain
-rw-r--r--	arith-int-056.cvc	812	log plain
-rw-r--r--	arith-int-057.cvc	805	log plain
-rw-r--r--	arith-int-058.cvc	814	log plain
-rw-r--r--	arith-int-059.cvc	810	log plain
-rw-r--r--	arith-int-060.cvc	801	log plain
-rw-r--r--	arith-int-061.cvc	1303	log plain
-rw-r--r--	arith-int-062.cvc	1306	log plain
-rw-r--r--	arith-int-063.cvc	1291	log plain
-rw-r--r--	arith-int-064.cvc	1309	log plain
-rw-r--r--	arith-int-065.cvc	1306	log plain
-rw-r--r--	arith-int-066.cvc	918	log plain
-rw-r--r--	arith-int-067.cvc	925	log plain
-rw-r--r--	arith-int-068.cvc	930	log plain
-rw-r--r--	arith-int-069.cvc	928	log plain
-rw-r--r--	arith-int-070.cvc	927	log plain
-rw-r--r--	arith-int-071.cvc	990	log plain
-rw-r--r--	arith-int-072.cvc	989	log plain
-rw-r--r--	arith-int-073.cvc	981	log plain
-rw-r--r--	arith-int-074.cvc	998	log plain
-rw-r--r--	arith-int-075.cvc	986	log plain
-rw-r--r--	arith-int-076.cvc	560	log plain
-rw-r--r--	arith-int-077.cvc	547	log plain
-rw-r--r--	arith-int-078.cvc	549	log plain
-rw-r--r--	arith-int-080.cvc	555	log plain
-rw-r--r--	arith-int-081.cvc	305	log plain
-rw-r--r--	arith-int-082.cvc	303	log plain
-rw-r--r--	arith-int-083.cvc	307	log plain
-rw-r--r--	arith-int-084.cvc	307	log plain
-rw-r--r--	arith-int-085.cvc	326	log plain
-rw-r--r--	arith-int-086.cvc	672	log plain
-rw-r--r--	arith-int-087.cvc	678	log plain
-rw-r--r--	arith-int-088.cvc	675	log plain
-rw-r--r--	arith-int-089.cvc	677	log plain
-rw-r--r--	arith-int-090.cvc	687	log plain
-rw-r--r--	arith-int-091.cvc	1233	log plain
-rw-r--r--	arith-int-092.cvc	1237	log plain
-rw-r--r--	arith-int-093.cvc	1239	log plain
-rw-r--r--	arith-int-094.cvc	1249	log plain
-rw-r--r--	arith-int-095.cvc	1245	log plain
-rw-r--r--	arith-int-096.cvc	365	log plain
-rw-r--r--	arith-int-097.cvc	369	log plain
-rw-r--r--	arith-int-099.cvc	375	log plain
-rw-r--r--	arith-int-100.cvc	373	log plain
-rw-r--r--	bug547.1.smt2	177	log plain
-rw-r--r--	bug716.0.smt2	22328	log plain
-rw-r--r--	bug716.1.cvc	173	log plain
-rw-r--r--	div.03.smt2	212	log plain
-rw-r--r--	div.06.smt2	256	log plain
-rw-r--r--	div.08.smt2	254	log plain
-rw-r--r--	div.09.smt2	388	log plain
-rw-r--r--	issue3952-rew-eq.smt2	1645	log plain
-rw-r--r--	issue789.smt2	2784	log plain
-rw-r--r--	miplib3.cvc	983	log plain
-rw-r--r--	mod.02.smt2	178	log plain
-rw-r--r--	mod.03.smt2	198	log plain
-rw-r--r--	mult.02.smt2	339	log plain
-rw-r--r--	pbrewrites-test.smt2	78967	log plain
-rw-r--r--	problem__003.smt2	3195	log plain