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--	Makefile	133	log plain
-rw-r--r--	Makefile.am	3989	log plain
d---------	arith	1722	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
-rw-r--r--	arrayinuf_declare.smt2	97	log plain
-rw-r--r--	arrayinuf_error.smt2	288	log plain
d---------	arrays	1059	log plain
d---------	aufbv	2171	log plain
d---------	auflia	634	log plain
-rw-r--r--	boolean-prec.cvc	154	log plain
-rw-r--r--	boolean-terms-kernel1.smt2	300	log plain
-rw-r--r--	boolean-terms-kernel2.smt2	735	log plain
-rw-r--r--	boolean-terms.cvc	254	log plain
-rw-r--r--	boolean.cvc	30119	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	60	log plain
-rw-r--r--	bug217.smt2	342	log plain
-rw-r--r--	bug220.smt2	17	log plain
-rw-r--r--	bug239.smt	5475	log plain
-rw-r--r--	bug274.cvc	1553	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	124	log plain
-rw-r--r--	bug32.cvc	65	log plain
-rw-r--r--	bug322.cvc	998	log plain
-rw-r--r--	bug322b.cvc	233	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	339	log plain
-rw-r--r--	bug383.smt2	159	log plain
-rw-r--r--	bug398.smt2	60	log plain
-rw-r--r--	bug421.smt2	267	log plain
-rw-r--r--	bug421b.smt2	460	log plain
-rw-r--r--	bug425.cvc	188769	log plain
-rw-r--r--	bug472.smt2	177	log plain
-rw-r--r--	bug480.smt2	312	log plain
-rw-r--r--	bug484.smt2	1944	log plain
-rw-r--r--	bug486.cvc	632	log plain
-rw-r--r--	bug49.smt	2386	log plain
-rw-r--r--	bug507.smt2	40893	log plain
-rw-r--r--	bug512.minimized.smt2	218	log plain
-rw-r--r--	bug512.smt2	4853	log plain
-rw-r--r--	bug516.smt2	298	log plain
-rw-r--r--	bug519.smt2	1903	log plain
-rw-r--r--	bug520.smt2	5568	log plain
-rw-r--r--	bug521.minimized.smt2	1887	log plain
-rw-r--r--	bug521.smt2	15189	log plain
-rw-r--r--	bug522.smt2	200	log plain
-rw-r--r--	bug528a.smt2	174	log plain
-rw-r--r--	bug541.smt2	180	log plain
-rw-r--r--	bug543.smt2	7348	log plain
-rw-r--r--	bug544.smt2	250	log plain
-rw-r--r--	bug548a.smt2	407	log plain
-rw-r--r--	bug567.smt2	2558	log plain
-rw-r--r--	buggy-ite.smt2	355	log plain
d---------	bv	4051	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	196	log plain
d---------	datatypes	1928	log plain
d---------	decision	2164	log plain
-rw-r--r--	distinct.smt	178	log plain
-rw-r--r--	error.cvc	215	log plain
-rw-r--r--	errorcrash.smt2	255	log plain
-rw-r--r--	flet.smt	140	log plain
-rw-r--r--	flet2.smt	126	log plain
d---------	fmf	797	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	304	log plain
-rw-r--r--	hole6.cvc	4656	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	79	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--	ite5.smt2	609	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	98	log plain
-rw-r--r--	let.smt	141	log plain
-rw-r--r--	let2.smt	126	log plain
-rw-r--r--	logops.01.cvc	86	log plain
-rw-r--r--	logops.02.cvc	55	log plain
-rw-r--r--	logops.03.cvc	101	log plain
-rw-r--r--	logops.04.cvc	67	log plain
-rw-r--r--	logops.05.cvc	58	log plain
-rw-r--r--	parallel-let.smt2	184	log plain
d---------	parser	130	log plain
d---------	precedence	801	log plain
d---------	preprocess	795	log plain
-rw-r--r--	print_lambda.cvc	163	log plain
d---------	push-pop	641	log plain
d---------	quantifiers	1794	log plain
-rw-r--r--	queries0.cvc	178	log plain
d---------	rewriterules	2820	log plain
d---------	sets	1526	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	133	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	129	log plain
-rw-r--r--	simplification_bug4.smt2	10582	log plain
-rw-r--r--	simplification_bug4.smt2.expect	46	log plain
-rw-r--r--	smallcnf.cvc	138	log plain
-rw-r--r--	smt2output.smt2	380	log plain
d---------	strings	1373	log plain
-rw-r--r--	subranges.cvc	189	log plain
-rw-r--r--	symmetric.smt	178	log plain
-rw-r--r--	test11.cvc	85	log plain
-rw-r--r--	test12.cvc	3056	log plain
-rw-r--r--	test9.cvc	62	log plain
d---------	tptp	1362	log plain
d---------	uf	1471	log plain
-rw-r--r--	uf20-03.cvc	3390	log plain
d---------	uflia	2187	log plain
d---------	uflra	1070	log plain
d---------	unconstrained	2028	log plain
-rw-r--r--	wiki.01.cvc	75	log plain
-rw-r--r--	wiki.02.cvc	79	log plain
-rw-r--r--	wiki.03.cvc	61	log plain
-rw-r--r--	wiki.04.cvc	63	log plain
-rw-r--r--	wiki.05.cvc	64	log plain
-rw-r--r--	wiki.06.cvc	64	log plain
-rw-r--r--	wiki.07.cvc	84	log plain
-rw-r--r--	wiki.08.cvc	85	log plain
-rw-r--r--	wiki.09.cvc	54	log plain
-rw-r--r--	wiki.10.cvc	65	log plain
-rw-r--r--	wiki.11.cvc	56	log plain
-rw-r--r--	wiki.12.cvc	57	log plain
-rw-r--r--	wiki.13.cvc	60	log plain
-rw-r--r--	wiki.14.cvc	60	log plain
-rw-r--r--	wiki.15.cvc	62	log plain
-rw-r--r--	wiki.16.cvc	65	log plain
-rw-r--r--	wiki.17.cvc	62	log plain
-rw-r--r--	wiki.18.cvc	62	log plain
-rw-r--r--	wiki.19.cvc	76	log plain
-rw-r--r--	wiki.20.cvc	76	log plain
-rw-r--r--	wiki.21.cvc	59	log plain