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--	GEO123+1.minimized.smt2	63186	log plain
-rw-r--r--	Makefile	133	log plain
-rw-r--r--	Makefile.am	3542	log plain
d---------	arith	1615	log plain
-rw-r--r--	arr1.smt	186	log plain
-rw-r--r--	arr1.smt2	260	log plain
-rw-r--r--	arr2.smt	213	log plain
d---------	arrays	1059	log plain
d---------	aufbv	2171	log plain
d---------	auflia	672	log plain
-rw-r--r--	boolean-prec.cvc	165	log plain
-rw-r--r--	boolean-terms.cvc	265	log plain
-rw-r--r--	boolean.cvc	30138	log plain
-rw-r--r--	bug161.smt	189	log plain
-rw-r--r--	bug164.smt	256	log plain
-rw-r--r--	bug167.smt	398	log plain
-rw-r--r--	bug168.smt	128	log plain
-rw-r--r--	bug187.smt2	123	log plain
-rw-r--r--	bug2.smt	513595	log plain
-rw-r--r--	bug216.smt2	189	log plain
-rw-r--r--	bug216.smt2.expect	71	log plain
-rw-r--r--	bug217.smt2	353	log plain
-rw-r--r--	bug220.smt2	17	log plain
-rw-r--r--	bug239.smt	5475	log plain
-rw-r--r--	bug274.cvc	1564	log plain
-rw-r--r--	bug288.smt	111	log plain
-rw-r--r--	bug288b.smt	118	log plain
-rw-r--r--	bug288c.smt	166	log plain
-rw-r--r--	bug296.smt2	73377	log plain
-rw-r--r--	bug303.smt2	461	log plain
-rw-r--r--	bug310.cvc	135	log plain
-rw-r--r--	bug32.cvc	76	log plain
-rw-r--r--	bug322.cvc	1009	log plain
-rw-r--r--	bug322b.cvc	244	log plain
-rw-r--r--	bug339.smt2	203	log plain
-rw-r--r--	bug365.smt2	149	log plain
-rw-r--r--	bug374.delta01.smt	38557	log plain
-rw-r--r--	bug374.smt	38557	log plain
-rw-r--r--	bug382.smt2	350	log plain
-rw-r--r--	bug383.smt2	159	log plain
-rw-r--r--	bug398.smt2	60	log plain
-rw-r--r--	bug411.smt2	191	log plain
-rw-r--r--	bug421.smt2	278	log plain
-rw-r--r--	bug421b.smt2	471	log plain
-rw-r--r--	bug425.cvc	188810	log plain
-rw-r--r--	bug472.smt2	177	log plain
-rw-r--r--	bug480.smt2	323	log plain
-rw-r--r--	bug484.smt2	1944	log plain
-rw-r--r--	bug486.cvc	643	log plain
-rw-r--r--	bug49.smt	2386	log plain
-rw-r--r--	bug497.cvc	107613	log plain
-rw-r--r--	bug507.smt2	40893	log plain
-rw-r--r--	bug512.minimized.smt2	194	log plain
-rw-r--r--	bug512.smt2	4861	log plain
-rw-r--r--	buggy-ite.smt2	355	log plain
d---------	bv	3921	log plain
-rw-r--r--	chained-equality.smt2	208	log plain
-rw-r--r--	constant-rewrite.smt	161	log plain
-rw-r--r--	cvc3-bug15.cvc	207	log plain
d---------	datatypes	1889	log plain
d---------	decision	2352	log plain
-rw-r--r--	distinct.smt	178	log plain
-rw-r--r--	error.cvc	127	log plain
-rw-r--r--	flet.smt	140	log plain
-rw-r--r--	flet2.smt	126	log plain
-rw-r--r--	fuzz_1.smt	742	log plain
-rw-r--r--	fuzz_3.smt	1155	log plain
-rw-r--r--	get-value-incremental.smt2	315	log plain
-rw-r--r--	hole6.cvc	4675	log plain
-rw-r--r--	hung10_itesdk_output1.smt2	920	log plain
-rw-r--r--	hung10_itesdk_output2.smt2	920	log plain
-rw-r--r--	hung13sdk_output1.smt2	425	log plain
-rw-r--r--	hung13sdk_output2.smt2	425	log plain
-rw-r--r--	incorrect1.smt	1891	log plain
-rw-r--r--	ineq_basic.smt	115	log plain
-rw-r--r--	ineq_slack.smt	158	log plain
-rw-r--r--	ite.cvc	90	log plain
-rw-r--r--	ite.smt2	152	log plain
-rw-r--r--	ite2.smt2	138	log plain
-rw-r--r--	ite3.smt2	199	log plain
-rw-r--r--	ite4.smt2	197	log plain
-rw-r--r--	ite_arith.smt2	140	log plain
-rw-r--r--	ite_real_int_type.smt	207	log plain
-rw-r--r--	ite_real_valid.smt	150	log plain
d---------	lemmas	548	log plain
-rw-r--r--	let.cvc	109	log plain
-rw-r--r--	let.smt	141	log plain
-rw-r--r--	let2.smt	126	log plain
-rw-r--r--	logops.01.cvc	97	log plain
-rw-r--r--	logops.02.cvc	66	log plain
-rw-r--r--	logops.03.cvc	112	log plain
-rw-r--r--	logops.04.cvc	78	log plain
-rw-r--r--	logops.05.cvc	69	log plain
-rw-r--r--	parallel-let.smt2	184	log plain
d---------	precedence	801	log plain
d---------	preprocess	795	log plain
-rw-r--r--	print_lambda.cvc	174	log plain
d---------	push-pop	680	log plain
d---------	quantifiers	1748	log plain
-rw-r--r--	queries0.cvc	189	log plain
d---------	rewriterules	2782	log plain
-rw-r--r--	simple-lra.smt	166	log plain
-rw-r--r--	simple-lra.smt2	174	log plain
-rw-r--r--	simple-rdl-definefun.smt2	552	log plain
-rw-r--r--	simple-rdl.smt	138	log plain
-rw-r--r--	simple-rdl.smt2	147	log plain
-rw-r--r--	simple-uf.smt	176	log plain
-rw-r--r--	simple-uf.smt2	201	log plain
-rw-r--r--	simple.cvc	144	log plain
-rw-r--r--	simple.smt	218	log plain
-rw-r--r--	simple2.smt	200	log plain
-rw-r--r--	simplification_bug.smt	101	log plain
-rw-r--r--	simplification_bug2.smt	102	log plain
-rw-r--r--	simplification_bug3.cvc	140	log plain
-rw-r--r--	simplification_bug4.smt2	10582	log plain
-rw-r--r--	simplification_bug4.smt2.expect	57	log plain
-rw-r--r--	smallcnf.cvc	149	log plain
-rw-r--r--	smt2output.smt2	391	log plain
-rw-r--r--	subranges.cvc	200	log plain
-rw-r--r--	symmetric.smt	178	log plain
-rw-r--r--	test11.cvc	96	log plain
-rw-r--r--	test12.cvc	3067	log plain
-rw-r--r--	test9.cvc	73	log plain
-rw-r--r--	tptp_parser.p	358	log plain
-rw-r--r--	tptp_parser10.p	280	log plain
-rw-r--r--	tptp_parser2.p	313	log plain
-rw-r--r--	tptp_parser3.p	327	log plain
-rw-r--r--	tptp_parser4.p	327	log plain
-rw-r--r--	tptp_parser5.p	358	log plain
-rw-r--r--	tptp_parser6.p	372	log plain
-rw-r--r--	tptp_parser7.p	358	log plain
-rw-r--r--	tptp_parser8.p	289	log plain
-rw-r--r--	tptp_parser9.p	340	log plain
d---------	uf	1431	log plain
-rw-r--r--	uf20-03.cvc	3401	log plain
d---------	uflia	2423	log plain
d---------	uflra	1192	log plain
d---------	unconstrained	1992	log plain
-rw-r--r--	wiki.01.cvc	86	log plain
-rw-r--r--	wiki.02.cvc	90	log plain
-rw-r--r--	wiki.03.cvc	72	log plain
-rw-r--r--	wiki.04.cvc	74	log plain
-rw-r--r--	wiki.05.cvc	83	log plain
-rw-r--r--	wiki.06.cvc	75	log plain
-rw-r--r--	wiki.07.cvc	95	log plain
-rw-r--r--	wiki.08.cvc	96	log plain
-rw-r--r--	wiki.09.cvc	65	log plain
-rw-r--r--	wiki.10.cvc	76	log plain
-rw-r--r--	wiki.11.cvc	67	log plain
-rw-r--r--	wiki.12.cvc	68	log plain
-rw-r--r--	wiki.13.cvc	71	log plain
-rw-r--r--	wiki.14.cvc	71	log plain
-rw-r--r--	wiki.15.cvc	73	log plain
-rw-r--r--	wiki.16.cvc	76	log plain
-rw-r--r--	wiki.17.cvc	73	log plain
-rw-r--r--	wiki.18.cvc	73	log plain
-rw-r--r--	wiki.19.cvc	87	log plain
-rw-r--r--	wiki.20.cvc	87	log plain
-rw-r--r--	wiki.21.cvc	70	log plain