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

drwxr-xr-x		..
drwxr-xr-x	-	arith	tree \| history
-rw-r--r--	260	arr1.smt2	blob \| history \| raw
-rw-r--r--	295	arr1.smtv1.smt2	blob \| history \| raw
-rw-r--r--	337	arr2.smtv1.smt2	blob \| history \| raw
-rw-r--r--	232	array-const-real-parse.smt2	blob \| history \| raw
-rw-r--r--	97	arrayinuf_declare.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--	157	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--	254	boolean-terms.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--	278	bug1247.smt2	blob \| history \| raw
-rw-r--r--	158	bug161.smtv1.smt2	blob \| history \| raw
-rw-r--r--	286	bug164.smtv1.smt2	blob \| history \| raw
-rw-r--r--	465	bug167.smtv1.smt2	blob \| history \| raw
-rw-r--r--	142	bug168.smtv1.smt2	blob \| history \| raw
-rw-r--r--	123	bug187.smt2	blob \| history \| raw
-rw-r--r--	494974	bug2.smtv1.smt2	blob \| history \| raw
-rw-r--r--	388	bug217.smt2	blob \| history \| raw
-rw-r--r--	17	bug220.smt2	blob \| history \| raw
-rw-r--r--	3635	bug239.smtv1.smt2	blob \| history \| raw
-rw-r--r--	1553	bug274.cvc	blob \| history \| raw
-rw-r--r--	160	bug288.smtv1.smt2	blob \| history \| raw
-rw-r--r--	166	bug288b.smtv1.smt2	blob \| history \| raw
-rw-r--r--	215	bug288c.smtv1.smt2	blob \| history \| raw
-rw-r--r--	461	bug303.smt2	blob \| history \| raw
-rw-r--r--	127	bug310.cvc	blob \| history \| raw
-rw-r--r--	68	bug32.cvc	blob \| history \| raw
-rw-r--r--	998	bug322.cvc	blob \| history \| raw
-rw-r--r--	242	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--	1072226	bug374.smtv1.smt2	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--	312	bug480.smt2	blob \| history \| raw
-rw-r--r--	1979	bug484.smt2	blob \| history \| raw
-rw-r--r--	640	bug486.cvc	blob \| history \| raw
-rw-r--r--	2428	bug49.smtv1.smt2	blob \| history \| raw
-rw-r--r--	218	bug512.minimized.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--	210	bug541.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--	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--	533	bug586.cvc	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--	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--	184	constant-rewrite.smtv1.smt2	blob \| history \| raw
-rw-r--r--	205	cvc-rerror-print.cvc	blob \| history \| raw
-rw-r--r--	199	cvc3-bug15.cvc	blob \| history \| raw
-rw-r--r--	632	cvc3.userdoc.01.cvc	blob \| history \| raw
-rw-r--r--	160	cvc3.userdoc.02.cvc	blob \| history \| raw
-rw-r--r--	200	cvc3.userdoc.03.cvc	blob \| history \| raw
-rw-r--r--	145	cvc3.userdoc.04.cvc	blob \| history \| raw
-rw-r--r--	243	cvc3.userdoc.05.cvc	blob \| history \| raw
-rw-r--r--	198	cvc3.userdoc.06.cvc	blob \| history \| raw
drwxr-xr-x	-	datatypes	tree \| history
drwxr-xr-x	-	decision	tree \| history
-rw-r--r--	217	declare-fun-is-match.smt2	blob \| history \| raw
-rw-r--r--	103	declare-funs.smt2	blob \| history \| raw
-rw-r--r--	397	define-fun-model.smt2	blob \| history \| raw
-rw-r--r--	257	distinct.smtv1.smt2	blob \| history \| raw
drwxr-xr-x	-	expect	tree \| history
-rw-r--r--	204	flet.smtv1.smt2	blob \| history \| raw
-rw-r--r--	190	flet2.smtv1.smt2	blob \| history \| raw
drwxr-xr-x	-	fmf	tree \| history
drwxr-xr-x	-	fp	tree \| history
-rw-r--r--	849	fuzz_1.smtv1.smt2	blob \| history \| raw
-rw-r--r--	652	fuzz_3.smtv1.smt2	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--	882	get-value-reals-ints.smt2	blob \| history \| raw
-rw-r--r--	635	get-value-reals.smt2	blob \| history \| raw
drwxr-xr-x	-	ho	tree \| history
-rw-r--r--	920	hung10_itesdk_output1.smt2	blob \| history \| raw
-rw-r--r--	425	hung13sdk_output1.smt2	blob \| history \| raw
-rw-r--r--	1454	incorrect1.smtv1.smt2	blob \| history \| raw
-rw-r--r--	152	ineq_basic.smtv1.smt2	blob \| history \| raw
-rw-r--r--	193	ineq_slack.smtv1.smt2	blob \| history \| raw
-rw-r--r--	444	issue1063-overloading-dt-cons.smt2	blob \| history \| raw
-rw-r--r--	329	issue1063-overloading-dt-fun.smt2	blob \| history \| raw
-rw-r--r--	320	issue1063-overloading-dt-sel.smt2	blob \| history \| raw
-rw-r--r--	295	issue2832-qualId.smt2	blob \| history \| raw
-rw-r--r--	151	issue4010-sort-inf-var.smt2	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--	140	ite_arith.smt2	blob \| history \| raw
-rw-r--r--	244	ite_real_int_type.smtv1.smt2	blob \| history \| raw
-rw-r--r--	195	ite_real_valid.smtv1.smt2	blob \| history \| raw
-rw-r--r--	249	lang_opts_2_5.smt2	blob \| history \| raw
-rw-r--r--	253	lang_opts_2_6_1.smt2	blob \| history \| raw
drwxr-xr-x	-	lemmas	tree \| history
-rw-r--r--	101	let.cvc	blob \| history \| raw
-rw-r--r--	234	let.smtv1.smt2	blob \| history \| raw
-rw-r--r--	197	let2.smtv1.smt2	blob \| history \| raw
-rw-r--r--	89	logops.01.cvc	blob \| history \| raw
-rw-r--r--	60	logops.02.cvc	blob \| history \| raw
-rw-r--r--	104	logops.03.cvc	blob \| history \| raw
-rw-r--r--	70	logops.04.cvc	blob \| history \| raw
-rw-r--r--	61	logops.05.cvc	blob \| history \| raw
-rw-r--r--	305	model-core.smt2	blob \| history \| raw
drwxr-xr-x	-	nl	tree \| history
-rw-r--r--	129	opt-abd-no-use.smt2	blob \| history \| raw
drwxr-xr-x	-	options	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--	308	print_lambda.cvc	blob \| history \| raw
-rw-r--r--	236	print_model.cvc	blob \| history \| raw
drwxr-xr-x	-	printer	tree \| history
-rw-r--r--	329	proof_no_support.smt2	blob \| history \| raw
drwxr-xr-x	-	push-pop	tree \| history
drwxr-xr-x	-	quantifiers	tree \| history
-rw-r--r--	197	rec-fun-const-parse-bug.smt2	blob \| history \| raw
drwxr-xr-x	-	rels	tree \| history
drwxr-xr-x	-	sep	tree \| history
drwxr-xr-x	-	sets	tree \| history
-rw-r--r--	174	simple-lra.smt2	blob \| history \| raw
-rw-r--r--	216	simple-lra.smtv1.smt2	blob \| history \| raw
-rw-r--r--	147	simple-rdl.smt2	blob \| history \| raw
-rw-r--r--	184	simple-rdl.smtv1.smt2	blob \| history \| raw
-rw-r--r--	201	simple-uf.smt2	blob \| history \| raw
-rw-r--r--	256	simple-uf.smtv1.smt2	blob \| history \| raw
-rw-r--r--	136	simple.cvc	blob \| history \| raw
-rw-r--r--	285	simple.smtv1.smt2	blob \| history \| raw
-rw-r--r--	277	simple2.smtv1.smt2	blob \| history \| raw
-rw-r--r--	139	simplification_bug.smtv1.smt2	blob \| history \| raw
-rw-r--r--	168	simplification_bug2.smtv1.smt2	blob \| history \| raw
-rw-r--r--	143	smallcnf.cvc	blob \| history \| raw
-rw-r--r--	380	smt2output.smt2	blob \| history \| raw
drwxr-xr-x	-	smtlib	tree \| history
drwxr-xr-x	-	strings	tree \| history
drwxr-xr-x	-	sygus	tree \| history
-rw-r--r--	249	symmetric.smtv1.smt2	blob \| history \| raw
-rw-r--r--	88	test11.cvc	blob \| history \| raw
-rw-r--r--	65	test9.cvc	blob \| history \| raw
drwxr-xr-x	-	tptp	tree \| history
drwxr-xr-x	-	uf	tree \| history
-rw-r--r--	3395	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--	78	wiki.01.cvc	blob \| history \| raw
-rw-r--r--	82	wiki.02.cvc	blob \| history \| raw
-rw-r--r--	64	wiki.03.cvc	blob \| history \| raw
-rw-r--r--	66	wiki.04.cvc	blob \| history \| raw
-rw-r--r--	67	wiki.05.cvc	blob \| history \| raw
-rw-r--r--	67	wiki.06.cvc	blob \| history \| raw
-rw-r--r--	87	wiki.07.cvc	blob \| history \| raw
-rw-r--r--	88	wiki.08.cvc	blob \| history \| raw
-rw-r--r--	57	wiki.09.cvc	blob \| history \| raw
-rw-r--r--	68	wiki.10.cvc	blob \| history \| raw
-rw-r--r--	59	wiki.11.cvc	blob \| history \| raw
-rw-r--r--	60	wiki.12.cvc	blob \| history \| raw
-rw-r--r--	63	wiki.13.cvc	blob \| history \| raw
-rw-r--r--	63	wiki.14.cvc	blob \| history \| raw
-rw-r--r--	65	wiki.15.cvc	blob \| history \| raw
-rw-r--r--	68	wiki.16.cvc	blob \| history \| raw
-rw-r--r--	65	wiki.17.cvc	blob \| history \| raw
-rw-r--r--	65	wiki.18.cvc	blob \| history \| raw
-rw-r--r--	79	wiki.19.cvc	blob \| history \| raw
-rw-r--r--	79	wiki.20.cvc	blob \| history \| raw
-rw-r--r--	62	wiki.21.cvc	blob \| history \| raw