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	4294	log plain
d---------	arith	1803	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	258	log plain
d---------	arrays	1440	log plain
d---------	aufbv	2217	log plain
d---------	auflia	595	log plain
-rw-r--r--	boolean-prec.cvc	154	log plain
-rw-r--r--	boolean-terms-bug-array.smt2	181	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--	bt-test-00.smt2	395	log plain
-rw-r--r--	bt-test-01.smt2	422	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	344	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	73367	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	309	log plain
-rw-r--r--	bug421b.smt2	502	log plain
-rw-r--r--	bug472.smt2	177	log plain
-rw-r--r--	bug480.smt2	312	log plain
-rw-r--r--	bug484.smt2	1934	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--	bug520.smt2	5568	log plain
-rw-r--r--	bug521.minimized.smt2	1887	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	2556	log plain
-rw-r--r--	bug576.smt2	769	log plain
-rw-r--r--	bug576a.smt2	1841	log plain
-rw-r--r--	bug578.smt2	187	log plain
-rw-r--r--	bug585.cvc	186	log plain
-rw-r--r--	bug586.cvc	533	log plain
-rw-r--r--	bug590.smt2	1759	log plain
-rw-r--r--	bug590.smt2.expect	76	log plain
-rw-r--r--	bug593.smt2	321	log plain
-rw-r--r--	bug595.cvc	103	log plain
-rw-r--r--	bug596.cvc	111	log plain
-rw-r--r--	bug596b.cvc	93	log plain
-rw-r--r--	bug605.cvc	586	log plain
-rw-r--r--	buggy-ite.smt2	355	log plain
d---------	bv	4591	log plain
-rw-r--r--	chained-equality.smt2	208	log plain
-rw-r--r--	constant-rewrite.smt	161	log plain
-rw-r--r--	crash_burn_locusts.smt2	797	log plain
-rw-r--r--	cvc3-bug15.cvc	196	log plain
-rw-r--r--	cvc3.userdoc.01.cvc	602	log plain
-rw-r--r--	cvc3.userdoc.02.cvc	157	log plain
-rw-r--r--	cvc3.userdoc.03.cvc	197	log plain
-rw-r--r--	cvc3.userdoc.04.cvc	142	log plain
-rw-r--r--	cvc3.userdoc.05.cvc	240	log plain
-rw-r--r--	cvc3.userdoc.06.cvc	192	log plain
d---------	datatypes	2905	log plain
d---------	decision	2126	log plain
-rw-r--r--	declare-funs.smt2	103	log plain
-rw-r--r--	distinct.smt	178	log plain
-rw-r--r--	error.cvc	215	log plain
-rw-r--r--	errorcrash.smt2	249	log plain
d---------	expect	532	log plain
-rw-r--r--	flet.smt	140	log plain
-rw-r--r--	flet2.smt	126	log plain
d---------	fmf	2482	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--	get-value-ints.smt2	404	log plain
-rw-r--r--	get-value-reals-ints.smt2	869	log plain
-rw-r--r--	get-value-reals.smt2	622	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	365	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
d---------	nl	1293	log plain
-rw-r--r--	parallel-let.smt2	184	log plain
d---------	parser	257	log plain
d---------	precedence	801	log plain
d---------	preprocess	795	log plain
-rw-r--r--	print_lambda.cvc	163	log plain
d---------	push-pop	1193	log plain
d---------	quantifiers	3908	log plain
-rw-r--r--	queries0.cvc	178	log plain
d---------	rels	3688	log plain
d---------	rewriterules	2718	log plain
d---------	sep	1783	log plain
d---------	sets	2224	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_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	3095	log plain
-rw-r--r--	subranges.cvc	189	log plain
d---------	sygus	1650	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
-rw-r--r--	trim.cvc	983	log plain
d---------	uf	1729	log plain
-rw-r--r--	uf20-03.cvc	3390	log plain
d---------	uflia	2187	log plain
d---------	uflra	1070	log plain
d---------	unconstrained	2066	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