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--	Makefile	142	log plain
-rw-r--r--	Makefile.am	1542	log plain
-rw-r--r--	arith.01.cvc	74	log plain
-rw-r--r--	arith.02.cvc	83	log plain
-rw-r--r--	arith.03.cvc	91	log plain
-rw-r--r--	bug443.delta01.smt	846	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	175	log plain
-rw-r--r--	div.03.smt2	226	log plain
-rw-r--r--	div.04.smt2	246	log plain
-rw-r--r--	div.05.smt2	238	log plain
-rw-r--r--	div.06.smt2	274	log plain
-rw-r--r--	div.07.smt2	267	log plain
-rw-r--r--	div.08.smt2	254	log plain
-rw-r--r--	div.09.smt2	546	log plain
-rw-r--r--	fuzz_3-eq.smt	1151	log plain
-rw-r--r--	incorrect1.smt	13884	log plain
d---------	integers	4670	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	65	log plain
-rw-r--r--	miplib-opt1217--27.smt2	223962	log plain
-rw-r--r--	miplib-pp08a-3000.smt	123671	log plain
-rw-r--r--	miplib-pp08a-3000.smt.expect	65	log plain
-rw-r--r--	miplib-pp08a-3000.smt2	70471	log plain
-rw-r--r--	miplib.cvc	805	log plain
-rw-r--r--	miplib2.cvc	907	log plain
-rw-r--r--	miplib3.cvc	1001	log plain
-rw-r--r--	miplib4.cvc	379	log plain
-rw-r--r--	miplibtrick.smt	234	log plain
-rw-r--r--	mod.01.smt2	209	log plain
-rw-r--r--	mod.02.smt2	192	log plain
-rw-r--r--	mod.03.smt2	216	log plain
-rw-r--r--	mult.01.smt2	339	log plain
-rw-r--r--	mult.02.smt2	335	log plain
-rw-r--r--	problem__003.smt2	3195	log plain