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--	abduct-dt.smt2	267	log plain
d---------	arith	1401	log plain
-rw-r--r--	arrayinuf_error.smt2	285	log plain
d---------	aufbv	174	log plain
d---------	auflia	39	log plain
d---------	bags	594	log plain
-rw-r--r--	boolean-terms-kernel2.smt2	735	log plain
-rw-r--r--	boolean.cvc	30122	log plain
-rw-r--r--	bug296.smt2	73952	log plain
-rw-r--r--	bug425.cvc	188769	log plain
-rw-r--r--	bug472.smt2	177	log plain
-rw-r--r--	bug507.smt2	41207	log plain
-rw-r--r--	bug512.smt2	4853	log plain
-rw-r--r--	bug516.smt2	301	log plain
-rw-r--r--	bug519.smt2	1889	log plain
-rw-r--r--	bug520.smt2	5666	log plain
-rw-r--r--	bug521.smt2	15189	log plain
-rw-r--r--	bug543.smt2	7348	log plain
-rw-r--r--	bug567.smt2	2627	log plain
-rw-r--r--	bug590.smt2	1827	log plain
-rw-r--r--	bug593.smt2	321	log plain
-rw-r--r--	bug681.smt2	1511	log plain
-rw-r--r--	bug694-Unapply1.scala-0.smt2	2983	log plain
-rw-r--r--	bug800.smt2	6317	log plain
d---------	bv	985	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
d---------	cores	42	log plain
d---------	datatypes	594	log plain
d---------	decision	616	log plain
-rw-r--r--	error.cvc	252	log plain
-rw-r--r--	errorcrash.smt2	276	log plain
-rw-r--r--	fmf-fun-dbu.smt2	542	log plain
d---------	fmf	2492	log plain
d---------	fp	51	log plain
-rw-r--r--	gensys_brn001.smt2	37318	log plain
d---------	ho	787	log plain
-rw-r--r--	hole6.cvc	4659	log plain
-rw-r--r--	issue3970-nl-ext-purify.smt2	1336	log plain
-rw-r--r--	issue3990-sort-inference.smt2	1282	log plain
-rw-r--r--	issue4273-ext-rew-cache.smt2	9234	log plain
-rw-r--r--	issue4335-unsat-core.smt2	13377	log plain
-rw-r--r--	issue5101-alira-subtypes.smt2	374	log plain
-rw-r--r--	issue5739-rtf-processed.smt2	278	log plain
-rw-r--r--	ite5.smt2	609	log plain
d---------	lemmas	130	log plain
-rw-r--r--	model-blocker-simple.smt2	372	log plain
-rw-r--r--	model-blocker-values.smt2	518	log plain
d---------	nl	3327	log plain
-rw-r--r--	non-fatal-errors.smt2	578	log plain
-rw-r--r--	parsing_ringer.cvc	1758	log plain
-rw-r--r--	proof00.smt2	1911	log plain
d---------	proofs	193	log plain
d---------	push-pop	2565	log plain
d---------	quantifiers	7594	log plain
d---------	rels	1483	log plain
d---------	rr-verify	238	log plain
d---------	sep	1476	log plain
d---------	sets	2537	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	127	log plain
d---------	strings	7300	log plain
-rw-r--r--	sygus-abduct-ex1-grammar.smt2	733	log plain
-rw-r--r--	sygus-abduct-test-ccore.smt2	342	log plain
-rw-r--r--	sygus-abduct-test-user.smt2	950	log plain
-rw-r--r--	sygus-abduct-test.smt2	428	log plain
d---------	sygus	7403	log plain
d---------	sym	475	log plain
-rw-r--r--	test12.cvc	3196	log plain
-rw-r--r--	trim.cvc	983	log plain
-rw-r--r--	uf2.smt2	412	log plain
d---------	uflia	467	log plain
-rw-r--r--	wrong-qfabvfp-smtcomp2018.smt2	566	log plain