fmf « 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--	ALG008-1.smt2	3364	log plain
-rw-r--r--	Hoare-z3.931718.smtv1.smt2	2568	log plain
-rw-r--r--	LeftistHeap.scala-8-ncm.smt2	6815	log plain
-rw-r--r--	PUZ001+1.smt2	4423	log plain
-rw-r--r--	agree466.smt2	30428	log plain
-rw-r--r--	agree467.smt2	20347	log plain
-rw-r--r--	alg202+1.smt2	2171	log plain
-rw-r--r--	am-bad-model.cvc	625	log plain
-rw-r--r--	bound-int-alt.smt2	470	log plain
-rw-r--r--	bug0909.smt2	3545	log plain
-rw-r--r--	bug651.smt2	2427	log plain
-rw-r--r--	bug723-irrelevant-funs.smt2	7472	log plain
-rw-r--r--	bug764.smt2	718	log plain
-rw-r--r--	cons-sets-bounds.smt2	645	log plain
-rw-r--r--	constr-ground-to.smt2	1970	log plain
-rw-r--r--	datatypes-ufinite-nested.smt2	577	log plain
-rw-r--r--	datatypes-ufinite.smt2	561	log plain
-rw-r--r--	dt-proper-model.smt2	404	log plain
-rw-r--r--	fc-pigeonhole19.smt2	434	log plain
-rw-r--r--	fib-core.smt2	967	log plain
-rw-r--r--	fmf-bound-2dim.smt2	296	log plain
-rw-r--r--	fmf-bound-int.smt2	235	log plain
-rw-r--r--	fmf-fun-divisor-pp.smt2	322	log plain
-rw-r--r--	fmf-fun-no-elim-ext-arith.smt2	423	log plain
-rw-r--r--	fmf-fun-no-elim-ext-arith2.smt2	565	log plain
-rw-r--r--	fmf-strange-bounds.smt2	825	log plain
-rw-r--r--	forall_unit_data.smt2	279	log plain
-rw-r--r--	fore19-exp2-core.smt2	7028	log plain
-rw-r--r--	german169.smt2	6364	log plain
-rw-r--r--	german73.smt2	6557	log plain
-rw-r--r--	issue2034-preinit.smt2	345	log plain
-rw-r--r--	issue3587.smt2	287	log plain
-rw-r--r--	issue3615.smt2	180	log plain
-rw-r--r--	issue3626.smt2	149	log plain
-rw-r--r--	issue3689.smt2	253	log plain
-rw-r--r--	issue4068-si-qf.smt2	223	log plain
-rw-r--r--	issue4225-univ-fun.smt2	182	log plain
-rw-r--r--	issue916-fmf-or.smt2	1178	log plain
-rw-r--r--	jasmin-cdt-crash.smt2	4155	log plain
-rw-r--r--	ko-bound-set.cvc	213	log plain
-rw-r--r--	loopy_coda.smt2	1371	log plain
-rw-r--r--	lst-no-self-rev-exp.smt2	1196	log plain
-rw-r--r--	memory_model-R_cpp-dd.cvc	1206	log plain
-rw-r--r--	nlp042+1.smt2	6429	log plain
-rw-r--r--	nun-0208-to.smt2	7327	log plain
-rw-r--r--	pow2-bool.smt2	312	log plain
-rw-r--r--	radu-quant-set.smt2	378	log plain
-rw-r--r--	refcount24.cvc.smt2	2157	log plain
-rw-r--r--	sc-crash-052316.smt2	1122	log plain
-rw-r--r--	sort-inf-int-real.smt2	564	log plain
-rw-r--r--	sort-inf-int.smt2	370	log plain
-rw-r--r--	with-ind-104-core.smt2	5838	log plain