unconstrained « 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.smt2	502	log plain
-rw-r--r--	arith2.smt2	328	log plain
-rw-r--r--	arith3.smt2	351	log plain
-rw-r--r--	arith4.smt2	382	log plain
-rw-r--r--	arith5.smt2	453	log plain
-rw-r--r--	arith6.smt2	453	log plain
-rw-r--r--	arith7.smt2	301	log plain
-rw-r--r--	array1.smt2	478	log plain
-rw-r--r--	bvbool.smt2	834	log plain
-rw-r--r--	bvbool2.smt2	707	log plain
-rw-r--r--	bvbool3.smt2	882	log plain
-rw-r--r--	bvcmp.smt2	533	log plain
-rw-r--r--	bvconcat.smt2	877	log plain
-rw-r--r--	bvconcat2.smt2	736	log plain
-rw-r--r--	bvdiv.smt2	943	log plain
-rw-r--r--	bvext.smt2	533	log plain
-rw-r--r--	bvite.smt2	878	log plain
-rw-r--r--	bvmul.smt2	803	log plain
-rw-r--r--	bvmul2.smt2	743	log plain
-rw-r--r--	bvmul3.smt2	812	log plain
-rw-r--r--	bvnot.smt2	530	log plain
-rw-r--r--	bvsle.smt2	778	log plain
-rw-r--r--	bvsle2.smt2	807	log plain
-rw-r--r--	bvsle3.smt2	691	log plain
-rw-r--r--	bvsle4.smt2	807	log plain
-rw-r--r--	bvsle5.smt2	691	log plain
-rw-r--r--	bvslt.smt2	778	log plain
-rw-r--r--	bvslt2.smt2	807	log plain
-rw-r--r--	bvslt3.smt2	685	log plain
-rw-r--r--	bvslt4.smt2	807	log plain
-rw-r--r--	bvslt5.smt2	685	log plain
-rw-r--r--	bvule.smt2	778	log plain
-rw-r--r--	bvule2.smt2	805	log plain
-rw-r--r--	bvule3.smt2	689	log plain
-rw-r--r--	bvule4.smt2	808	log plain
-rw-r--r--	bvule5.smt2	692	log plain
-rw-r--r--	bvult.smt2	778	log plain
-rw-r--r--	bvult2.smt2	808	log plain
-rw-r--r--	bvult3.smt2	686	log plain
-rw-r--r--	bvult4.smt2	805	log plain
-rw-r--r--	bvult5.smt2	683	log plain
-rw-r--r--	files	561	log plain
-rw-r--r--	geq.smt2	487	log plain
-rw-r--r--	gt.smt2	486	log plain
-rw-r--r--	ite.smt2	284	log plain
-rw-r--r--	leq.smt2	487	log plain
-rw-r--r--	lt.smt2	486	log plain
-rw-r--r--	mult1.smt2	167	log plain
-rw-r--r--	uf1.smt2	449	log plain
-rw-r--r--	xor.smt2	953	log plain