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	412	log plain
-rw-r--r--	arith-int-004.cvc	739	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-022.cvc	119	log plain
-rw-r--r--	arith-int-024.cvc	116	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-050.cvc	242	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-097.cvc	369	log plain
-rw-r--r--	bug547.1.smt2	170	log plain
-rw-r--r--	bug716.0.smt2	22328	log plain
-rw-r--r--	bug716.1.cvc	189	log plain
-rw-r--r--	bug716.2.cvc	203	log plain
-rw-r--r--	div.03.smt2	212	log plain
-rw-r--r--	div.06.smt2	275	log plain
-rw-r--r--	div.08.smt2	254	log plain
-rw-r--r--	div.09.smt2	388	log plain
-rw-r--r--	issue3480.smt2	300	log plain
-rw-r--r--	issue3952-rew-eq.smt2	1645	log plain
-rw-r--r--	issue4985-model-success.smt2	289	log plain
-rw-r--r--	issue4985b-model-success.smt2	182	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	217	log plain
-rw-r--r--	mult.02.smt2	335	log plain
-rw-r--r--	pbrewrites-test.smt2	78967	log plain
-rw-r--r--	problem__003.smt2	3195	log plain