regress1 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
d---------	arith	4714	log plain
-rw-r--r--	arrayinuf_error.smt2	285	log plain
d---------	aufbv	77	log plain
d---------	auflia	78	log plain
-rw-r--r--	boolean-terms-kernel2.smt2	735	log plain
-rw-r--r--	boolean.cvc	30119	log plain
-rw-r--r--	bug216.smt2	250	log plain
-rw-r--r--	bug296.smt2	73413	log plain
-rw-r--r--	bug425.cvc	188769	log plain
-rw-r--r--	bug472.smt2	177	log plain
-rw-r--r--	bug507.smt2	40937	log plain
-rw-r--r--	bug512.smt2	4853	log plain
-rw-r--r--	bug516.smt2	298	log plain
-rw-r--r--	bug519.smt2	1906	log plain
-rw-r--r--	bug520.smt2	5631	log plain
-rw-r--r--	bug521.smt2	15189	log plain
-rw-r--r--	bug543.smt2	7348	log plain
-rw-r--r--	bug567.smt2	2570	log plain
-rw-r--r--	bug585.cvc	186	log plain
-rw-r--r--	bug590.smt2	1836	log plain
-rw-r--r--	bug593.smt2	321	log plain
-rw-r--r--	bug681.smt2	1539	log plain
-rw-r--r--	bug694-Unapply1.scala-0.smt2	2981	log plain
-rw-r--r--	bug800.smt2	6317	log plain
d---------	bv	688	log plain
-rw-r--r--	bvdiv2.smt2	721	log plain
-rw-r--r--	constarr3.cvc	367	log plain
-rw-r--r--	constarr3.smt2	553	log plain
-rw-r--r--	crash_burn_locusts.smt2	797	log plain
d---------	datatypes	235	log plain
d---------	decision	150	log plain
-rw-r--r--	error.cvc	253	log plain
-rw-r--r--	errorcrash.smt2	276	log plain
-rw-r--r--	fmf-fun-dbu.smt2	542	log plain
d---------	fmf	2108	log plain
-rw-r--r--	gensys_brn001.smt2	37318	log plain
d---------	ho	393	log plain
-rw-r--r--	hole6.cvc	4656	log plain
-rw-r--r--	issue1048-arrays-int-real.smt2	151	log plain
-rw-r--r--	ite5.smt2	609	log plain
d---------	lemmas	183	log plain
d---------	nl	2480	log plain
-rw-r--r--	non-fatal-errors.smt2	611	log plain
-rw-r--r--	parsing_ringer.cvc	1758	log plain
-rw-r--r--	proof00.smt2	1911	log plain
d---------	push-pop	2553	log plain
d---------	quantifiers	4435	log plain
d---------	rels	1577	log plain
d---------	rewriterules	1176	log plain
d---------	sep	1476	log plain
d---------	sets	1390	log plain
-rw-r--r--	simple-rdl-definefun.smt2	552	log plain
-rw-r--r--	simplification_bug4.smt2	10629	log plain
-rw-r--r--	sqrt2-sort-inf-unk.smt2	145	log plain
d---------	strings	3071	log plain
d---------	sygus	3530	log plain
d---------	sym	262	log plain
-rw-r--r--	test12.cvc	3056	log plain
-rw-r--r--	trim.cvc	983	log plain
-rw-r--r--	uf2.smt2	412	log plain
d---------	uflia	422	log plain
-rw-r--r--	wrong-qfabvfp-smtcomp2018.smt2	559	log plain