arith « 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--	arith.01.cvc	63	log plain
-rw-r--r--	arith.02.cvc	72	log plain
-rw-r--r--	arith.03.cvc	80	log plain
-rw-r--r--	bug443.delta01.smt	846	log plain
-rw-r--r--	bug547.2.smt2	187	log plain
-rw-r--r--	bug549.cvc	65	log plain
-rw-r--r--	bug569.smt2	340	log plain
-rw-r--r--	delta-minimized-row-vector-bug.smt	255	log plain
-rw-r--r--	div.01.smt2	296	log plain
-rw-r--r--	div.02.smt2	157	log plain
-rw-r--r--	div.04.smt2	246	log plain
-rw-r--r--	div.05.smt2	220	log plain
-rw-r--r--	div.07.smt2	267	log plain
-rw-r--r--	fuzz_3-eq.smt	1151	log plain
-rw-r--r--	incorrect1.smt	13884	log plain
d---------	integers	410	log plain
-rw-r--r--	leq.01.smt	71	log plain
-rw-r--r--	miplib-opt1217--27.smt	270139	log plain
-rw-r--r--	miplib-opt1217--27.smt.expect	47	log plain
-rw-r--r--	miplib-pp08a-3000.smt	123671	log plain
-rw-r--r--	miplib-pp08a-3000.smt.expect	47	log plain
-rw-r--r--	miplib.cvc	787	log plain
-rw-r--r--	miplib2.cvc	889	log plain
-rw-r--r--	miplib4.cvc	361	log plain
-rw-r--r--	miplibtrick.smt	234	log plain
-rw-r--r--	mod-simp.smt2	189	log plain
-rw-r--r--	mod.01.smt2	191	log plain
-rw-r--r--	mult.01.smt2	325	log plain