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-int-001.cvc	738	log plain
-rw-r--r--	arith-int-002.cvc	740	log plain
-rw-r--r--	arith-int-003.cvc	743	log plain
-rw-r--r--	arith-int-004.cvc	734	log plain
-rw-r--r--	arith-int-005.cvc	737	log plain
-rw-r--r--	arith-int-006.cvc	476	log plain
-rw-r--r--	arith-int-007.cvc	489	log plain
-rw-r--r--	arith-int-008.cvc	490	log plain
-rw-r--r--	arith-int-009.cvc	489	log plain
-rw-r--r--	arith-int-010.cvc	479	log plain
-rw-r--r--	arith-int-011.cvc	172	log plain
-rw-r--r--	arith-int-012.cvc	177	log plain
-rw-r--r--	arith-int-013.cvc	175	log plain
-rw-r--r--	arith-int-016.cvc	1105	log plain
-rw-r--r--	arith-int-017.cvc	1105	log plain
-rw-r--r--	arith-int-018.cvc	1120	log plain
-rw-r--r--	arith-int-019.cvc	1106	log plain
-rw-r--r--	arith-int-020.cvc	1103	log plain
-rw-r--r--	arith-int-022.cvc	114	log plain
-rw-r--r--	arith-int-024.cvc	111	log plain
-rw-r--r--	arith-int-026.cvc	1171	log plain
-rw-r--r--	arith-int-027.cvc	1175	log plain
-rw-r--r--	arith-int-028.cvc	1173	log plain
-rw-r--r--	arith-int-029.cvc	1178	log plain
-rw-r--r--	arith-int-030.cvc	1172	log plain
-rw-r--r--	arith-int-031.cvc	1061	log plain
-rw-r--r--	arith-int-032.cvc	1049	log plain
-rw-r--r--	arith-int-033.cvc	1043	log plain
-rw-r--r--	arith-int-034.cvc	1049	log plain
-rw-r--r--	arith-int-035.cvc	1042	log plain
-rw-r--r--	arith-int-036.cvc	862	log plain
-rw-r--r--	arith-int-037.cvc	869	log plain
-rw-r--r--	arith-int-038.cvc	856	log plain
-rw-r--r--	arith-int-039.cvc	859	log plain
-rw-r--r--	arith-int-040.cvc	866	log plain
-rw-r--r--	arith-int-041.cvc	427	log plain
-rw-r--r--	arith-int-043.cvc	424	log plain
-rw-r--r--	arith-int-044.cvc	463	log plain
-rw-r--r--	arith-int-045.cvc	419	log plain
-rw-r--r--	arith-int-046.cvc	238	log plain
-rw-r--r--	arith-int-047.cvc	239	log plain
-rw-r--r--	arith-int-048.cvc	237	log plain
-rw-r--r--	arith-int-049.cvc	242	log plain
-rw-r--r--	arith-int-050.cvc	237	log plain
-rw-r--r--	arith-int-051.cvc	611	log plain
-rw-r--r--	arith-int-052.cvc	610	log plain
-rw-r--r--	arith-int-053.cvc	602	log plain
-rw-r--r--	arith-int-054.cvc	610	log plain
-rw-r--r--	arith-int-055.cvc	612	log plain
-rw-r--r--	arith-int-056.cvc	809	log plain
-rw-r--r--	arith-int-057.cvc	802	log plain
-rw-r--r--	arith-int-058.cvc	811	log plain
-rw-r--r--	arith-int-059.cvc	807	log plain
-rw-r--r--	arith-int-060.cvc	798	log plain
-rw-r--r--	arith-int-061.cvc	1300	log plain
-rw-r--r--	arith-int-062.cvc	1303	log plain
-rw-r--r--	arith-int-063.cvc	1288	log plain
-rw-r--r--	arith-int-064.cvc	1306	log plain
-rw-r--r--	arith-int-065.cvc	1303	log plain
-rw-r--r--	arith-int-066.cvc	915	log plain
-rw-r--r--	arith-int-067.cvc	922	log plain
-rw-r--r--	arith-int-068.cvc	927	log plain
-rw-r--r--	arith-int-069.cvc	925	log plain
-rw-r--r--	arith-int-070.cvc	924	log plain
-rw-r--r--	arith-int-071.cvc	987	log plain
-rw-r--r--	arith-int-072.cvc	986	log plain
-rw-r--r--	arith-int-073.cvc	978	log plain
-rw-r--r--	arith-int-074.cvc	995	log plain
-rw-r--r--	arith-int-075.cvc	983	log plain
-rw-r--r--	arith-int-076.cvc	557	log plain
-rw-r--r--	arith-int-077.cvc	544	log plain
-rw-r--r--	arith-int-078.cvc	546	log plain
-rw-r--r--	arith-int-080.cvc	552	log plain
-rw-r--r--	arith-int-081.cvc	300	log plain
-rw-r--r--	arith-int-082.cvc	298	log plain
-rw-r--r--	arith-int-083.cvc	302	log plain
-rw-r--r--	arith-int-084.cvc	302	log plain
-rw-r--r--	arith-int-085.cvc	321	log plain
-rw-r--r--	arith-int-086.cvc	669	log plain
-rw-r--r--	arith-int-087.cvc	675	log plain
-rw-r--r--	arith-int-088.cvc	672	log plain
-rw-r--r--	arith-int-089.cvc	674	log plain
-rw-r--r--	arith-int-090.cvc	682	log plain
-rw-r--r--	arith-int-091.cvc	1230	log plain
-rw-r--r--	arith-int-092.cvc	1234	log plain
-rw-r--r--	arith-int-093.cvc	1236	log plain
-rw-r--r--	arith-int-094.cvc	1246	log plain
-rw-r--r--	arith-int-095.cvc	1242	log plain
-rw-r--r--	arith-int-096.cvc	360	log plain
-rw-r--r--	arith-int-097.cvc	364	log plain
-rw-r--r--	arith-int-099.cvc	370	log plain
-rw-r--r--	arith-int-100.cvc	368	log plain
-rw-r--r--	bug547.1.smt2	164	log plain
-rw-r--r--	bug716.0.smt2	22284	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--	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
-rw-r--r--	real2int-test.smt2	978	log plain