git.libre-soc.org Git - cvc5.git/tree - test/regress/regress0/

drwxr-xr-x		..
-rw-r--r--	133	Makefile	blob \| history \| raw
-rw-r--r--	4391	Makefile.am	blob \| history \| raw
drwxr-xr-x	-	arith	tree \| history
-rw-r--r--	186	arr1.smt	blob \| history \| raw
-rw-r--r--	260	arr1.smt2	blob \| history \| raw
-rw-r--r--	213	arr2.smt	blob \| history \| raw
-rw-r--r--	97	arrayinuf_declare.smt2	blob \| history \| raw
-rw-r--r--	258	arrayinuf_error.smt2	blob \| history \| raw
drwxr-xr-x	-	arrays	tree \| history
drwxr-xr-x	-	aufbv	tree \| history
drwxr-xr-x	-	auflia	tree \| history
-rw-r--r--	154	boolean-prec.cvc	blob \| history \| raw
-rw-r--r--	181	boolean-terms-bug-array.smt2	blob \| history \| raw
-rw-r--r--	300	boolean-terms-kernel1.smt2	blob \| history \| raw
-rw-r--r--	735	boolean-terms-kernel2.smt2	blob \| history \| raw
-rw-r--r--	254	boolean-terms.cvc	blob \| history \| raw
-rw-r--r--	30119	boolean.cvc	blob \| history \| raw
-rw-r--r--	395	bt-test-00.smt2	blob \| history \| raw
-rw-r--r--	422	bt-test-01.smt2	blob \| history \| raw
-rw-r--r--	189	bug161.smt	blob \| history \| raw
-rw-r--r--	256	bug164.smt	blob \| history \| raw
-rw-r--r--	398	bug167.smt	blob \| history \| raw
-rw-r--r--	128	bug168.smt	blob \| history \| raw
-rw-r--r--	123	bug187.smt2	blob \| history \| raw
-rw-r--r--	513595	bug2.smt	blob \| history \| raw
-rw-r--r--	189	bug216.smt2	blob \| history \| raw
-rw-r--r--	60	bug216.smt2.expect	blob \| history \| raw
-rw-r--r--	344	bug217.smt2	blob \| history \| raw
-rw-r--r--	17	bug220.smt2	blob \| history \| raw
-rw-r--r--	5475	bug239.smt	blob \| history \| raw
-rw-r--r--	1553	bug274.cvc	blob \| history \| raw
-rw-r--r--	111	bug288.smt	blob \| history \| raw
-rw-r--r--	118	bug288b.smt	blob \| history \| raw
-rw-r--r--	166	bug288c.smt	blob \| history \| raw
-rw-r--r--	73367	bug296.smt2	blob \| history \| raw
-rw-r--r--	461	bug303.smt2	blob \| history \| raw
-rw-r--r--	124	bug310.cvc	blob \| history \| raw
-rw-r--r--	65	bug32.cvc	blob \| history \| raw
-rw-r--r--	998	bug322.cvc	blob \| history \| raw
-rw-r--r--	233	bug322b.cvc	blob \| history \| raw
-rw-r--r--	203	bug339.smt2	blob \| history \| raw
-rw-r--r--	149	bug365.smt2	blob \| history \| raw
-rw-r--r--	38557	bug374.delta01.smt	blob \| history \| raw
-rw-r--r--	38557	bug374.smt	blob \| history \| raw
-rw-r--r--	339	bug382.smt2	blob \| history \| raw
-rw-r--r--	159	bug383.smt2	blob \| history \| raw
-rw-r--r--	60	bug398.smt2	blob \| history \| raw
-rw-r--r--	309	bug421.smt2	blob \| history \| raw
-rw-r--r--	502	bug421b.smt2	blob \| history \| raw
-rw-r--r--	177	bug472.smt2	blob \| history \| raw
-rw-r--r--	312	bug480.smt2	blob \| history \| raw
-rw-r--r--	1934	bug484.smt2	blob \| history \| raw
-rw-r--r--	632	bug486.cvc	blob \| history \| raw
-rw-r--r--	2386	bug49.smt	blob \| history \| raw
-rw-r--r--	40893	bug507.smt2	blob \| history \| raw
-rw-r--r--	218	bug512.minimized.smt2	blob \| history \| raw
-rw-r--r--	4853	bug512.smt2	blob \| history \| raw
-rw-r--r--	298	bug516.smt2	blob \| history \| raw
-rw-r--r--	5568	bug520.smt2	blob \| history \| raw
-rw-r--r--	1887	bug521.minimized.smt2	blob \| history \| raw
-rw-r--r--	200	bug522.smt2	blob \| history \| raw
-rw-r--r--	174	bug528a.smt2	blob \| history \| raw
-rw-r--r--	180	bug541.smt2	blob \| history \| raw
-rw-r--r--	7348	bug543.smt2	blob \| history \| raw
-rw-r--r--	250	bug544.smt2	blob \| history \| raw
-rw-r--r--	407	bug548a.smt2	blob \| history \| raw
-rw-r--r--	2556	bug567.smt2	blob \| history \| raw
-rw-r--r--	769	bug576.smt2	blob \| history \| raw
-rw-r--r--	1841	bug576a.smt2	blob \| history \| raw
-rw-r--r--	187	bug578.smt2	blob \| history \| raw
-rw-r--r--	186	bug585.cvc	blob \| history \| raw
-rw-r--r--	533	bug586.cvc	blob \| history \| raw
-rw-r--r--	1759	bug590.smt2	blob \| history \| raw
-rw-r--r--	76	bug590.smt2.expect	blob \| history \| raw
-rw-r--r--	321	bug593.smt2	blob \| history \| raw
-rw-r--r--	103	bug595.cvc	blob \| history \| raw
-rw-r--r--	111	bug596.cvc	blob \| history \| raw
-rw-r--r--	93	bug596b.cvc	blob \| history \| raw
-rw-r--r--	586	bug605.cvc	blob \| history \| raw
-rw-r--r--	858	bug639.smt2	blob \| history \| raw
-rw-r--r--	1509	bug681.smt2	blob \| history \| raw
-rw-r--r--	355	buggy-ite.smt2	blob \| history \| raw
drwxr-xr-x	-	bv	tree \| history
-rw-r--r--	208	chained-equality.smt2	blob \| history \| raw
-rw-r--r--	161	constant-rewrite.smt	blob \| history \| raw
-rw-r--r--	797	crash_burn_locusts.smt2	blob \| history \| raw
-rw-r--r--	196	cvc3-bug15.cvc	blob \| history \| raw
-rw-r--r--	602	cvc3.userdoc.01.cvc	blob \| history \| raw
-rw-r--r--	157	cvc3.userdoc.02.cvc	blob \| history \| raw
-rw-r--r--	197	cvc3.userdoc.03.cvc	blob \| history \| raw
-rw-r--r--	142	cvc3.userdoc.04.cvc	blob \| history \| raw
-rw-r--r--	240	cvc3.userdoc.05.cvc	blob \| history \| raw
-rw-r--r--	192	cvc3.userdoc.06.cvc	blob \| history \| raw
drwxr-xr-x	-	datatypes	tree \| history
drwxr-xr-x	-	decision	tree \| history
-rw-r--r--	193	declare-fun-is-match.smt2	blob \| history \| raw
-rw-r--r--	103	declare-funs.smt2	blob \| history \| raw
-rw-r--r--	178	distinct.smt	blob \| history \| raw
-rw-r--r--	215	error.cvc	blob \| history \| raw
-rw-r--r--	249	errorcrash.smt2	blob \| history \| raw
drwxr-xr-x	-	expect	tree \| history
-rw-r--r--	140	flet.smt	blob \| history \| raw
-rw-r--r--	126	flet2.smt	blob \| history \| raw
drwxr-xr-x	-	fmf	tree \| history
-rw-r--r--	742	fuzz_1.smt	blob \| history \| raw
-rw-r--r--	1155	fuzz_3.smt	blob \| history \| raw
-rw-r--r--	304	get-value-incremental.smt2	blob \| history \| raw
-rw-r--r--	404	get-value-ints.smt2	blob \| history \| raw
-rw-r--r--	869	get-value-reals-ints.smt2	blob \| history \| raw
-rw-r--r--	622	get-value-reals.smt2	blob \| history \| raw
-rw-r--r--	4656	hole6.cvc	blob \| history \| raw
-rw-r--r--	920	hung10_itesdk_output1.smt2	blob \| history \| raw
-rw-r--r--	920	hung10_itesdk_output2.smt2	blob \| history \| raw
-rw-r--r--	425	hung13sdk_output1.smt2	blob \| history \| raw
-rw-r--r--	425	hung13sdk_output2.smt2	blob \| history \| raw
-rw-r--r--	1891	incorrect1.smt	blob \| history \| raw
-rw-r--r--	115	ineq_basic.smt	blob \| history \| raw
-rw-r--r--	158	ineq_slack.smt	blob \| history \| raw
-rw-r--r--	79	ite.cvc	blob \| history \| raw
-rw-r--r--	152	ite.smt2	blob \| history \| raw
-rw-r--r--	138	ite2.smt2	blob \| history \| raw
-rw-r--r--	199	ite3.smt2	blob \| history \| raw
-rw-r--r--	197	ite4.smt2	blob \| history \| raw
-rw-r--r--	609	ite5.smt2	blob \| history \| raw
-rw-r--r--	140	ite_arith.smt2	blob \| history \| raw
-rw-r--r--	207	ite_real_int_type.smt	blob \| history \| raw
-rw-r--r--	150	ite_real_valid.smt	blob \| history \| raw
drwxr-xr-x	-	lemmas	tree \| history
-rw-r--r--	98	let.cvc	blob \| history \| raw
-rw-r--r--	141	let.smt	blob \| history \| raw
-rw-r--r--	126	let2.smt	blob \| history \| raw
-rw-r--r--	86	logops.01.cvc	blob \| history \| raw
-rw-r--r--	55	logops.02.cvc	blob \| history \| raw
-rw-r--r--	101	logops.03.cvc	blob \| history \| raw
-rw-r--r--	67	logops.04.cvc	blob \| history \| raw
-rw-r--r--	58	logops.05.cvc	blob \| history \| raw
drwxr-xr-x	-	nl	tree \| history
-rw-r--r--	184	parallel-let.smt2	blob \| history \| raw
drwxr-xr-x	-	parser	tree \| history
drwxr-xr-x	-	precedence	tree \| history
drwxr-xr-x	-	preprocess	tree \| history
-rw-r--r--	163	print_lambda.cvc	blob \| history \| raw
drwxr-xr-x	-	push-pop	tree \| history
drwxr-xr-x	-	quantifiers	tree \| history
-rw-r--r--	178	queries0.cvc	blob \| history \| raw
drwxr-xr-x	-	rels	tree \| history
drwxr-xr-x	-	rewriterules	tree \| history
drwxr-xr-x	-	sep	tree \| history
drwxr-xr-x	-	sets	tree \| history
-rw-r--r--	166	simple-lra.smt	blob \| history \| raw
-rw-r--r--	174	simple-lra.smt2	blob \| history \| raw
-rw-r--r--	552	simple-rdl-definefun.smt2	blob \| history \| raw
-rw-r--r--	138	simple-rdl.smt	blob \| history \| raw
-rw-r--r--	147	simple-rdl.smt2	blob \| history \| raw
-rw-r--r--	176	simple-uf.smt	blob \| history \| raw
-rw-r--r--	201	simple-uf.smt2	blob \| history \| raw
-rw-r--r--	133	simple.cvc	blob \| history \| raw
-rw-r--r--	218	simple.smt	blob \| history \| raw
-rw-r--r--	200	simple2.smt	blob \| history \| raw
-rw-r--r--	101	simplification_bug.smt	blob \| history \| raw
-rw-r--r--	102	simplification_bug2.smt	blob \| history \| raw
-rw-r--r--	10582	simplification_bug4.smt2	blob \| history \| raw
-rw-r--r--	46	simplification_bug4.smt2.expect	blob \| history \| raw
-rw-r--r--	138	smallcnf.cvc	blob \| history \| raw
-rw-r--r--	380	smt2output.smt2	blob \| history \| raw
drwxr-xr-x	-	strings	tree \| history
-rw-r--r--	189	subranges.cvc	blob \| history \| raw
drwxr-xr-x	-	sygus	tree \| history
-rw-r--r--	178	symmetric.smt	blob \| history \| raw
-rw-r--r--	85	test11.cvc	blob \| history \| raw
-rw-r--r--	3056	test12.cvc	blob \| history \| raw
-rw-r--r--	62	test9.cvc	blob \| history \| raw
drwxr-xr-x	-	tptp	tree \| history
-rw-r--r--	983	trim.cvc	blob \| history \| raw
drwxr-xr-x	-	uf	tree \| history
-rw-r--r--	3390	uf20-03.cvc	blob \| history \| raw
drwxr-xr-x	-	uflia	tree \| history
drwxr-xr-x	-	uflra	tree \| history
drwxr-xr-x	-	unconstrained	tree \| history
-rw-r--r--	75	wiki.01.cvc	blob \| history \| raw
-rw-r--r--	79	wiki.02.cvc	blob \| history \| raw
-rw-r--r--	61	wiki.03.cvc	blob \| history \| raw
-rw-r--r--	63	wiki.04.cvc	blob \| history \| raw
-rw-r--r--	64	wiki.05.cvc	blob \| history \| raw
-rw-r--r--	64	wiki.06.cvc	blob \| history \| raw
-rw-r--r--	84	wiki.07.cvc	blob \| history \| raw
-rw-r--r--	85	wiki.08.cvc	blob \| history \| raw
-rw-r--r--	54	wiki.09.cvc	blob \| history \| raw
-rw-r--r--	65	wiki.10.cvc	blob \| history \| raw
-rw-r--r--	56	wiki.11.cvc	blob \| history \| raw
-rw-r--r--	57	wiki.12.cvc	blob \| history \| raw
-rw-r--r--	60	wiki.13.cvc	blob \| history \| raw
-rw-r--r--	60	wiki.14.cvc	blob \| history \| raw
-rw-r--r--	62	wiki.15.cvc	blob \| history \| raw
-rw-r--r--	65	wiki.16.cvc	blob \| history \| raw
-rw-r--r--	62	wiki.17.cvc	blob \| history \| raw
-rw-r--r--	62	wiki.18.cvc	blob \| history \| raw
-rw-r--r--	76	wiki.19.cvc	blob \| history \| raw
-rw-r--r--	76	wiki.20.cvc	blob \| history \| raw
-rw-r--r--	59	wiki.21.cvc	blob \| history \| raw