git.libre-soc.org Git - cvc5.git/tree - test/regress/cli/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
drwxr-xr-x	-	bool	tree \| history
-rw-r--r--	230	boolean-prec.cvc.smt2	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--	215	boolean-terms.cvc.smt2	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--	344	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--	1540	bug274.cvc.smt2	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--	203	bug310.cvc.smt2	blob \| history \| raw
-rw-r--r--	163	bug32.cvc.smt2	blob \| history \| raw
-rw-r--r--	443	bug322.cvc.smt2	blob \| history \| raw
-rw-r--r--	404	bug322b.cvc.smt2	blob \| history \| raw
-rw-r--r--	205	bug339.smt2	blob \| history \| raw
-rw-r--r--	149	bug365.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--	64	bug398.smt2	blob \| history \| raw
-rw-r--r--	313	bug421.smt2	blob \| history \| raw
-rw-r--r--	312	bug480.smt2	blob \| history \| raw
-rw-r--r--	1923	bug484.smt2	blob \| history \| raw
-rw-r--r--	1069	bug486.cvc.smt2	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--	1877	bug521.minimized.smt2	blob \| history \| raw
-rw-r--r--	198	bug522.smt2	blob \| history \| raw
-rw-r--r--	203	bug528a.smt2	blob \| history \| raw
-rw-r--r--	182	bug541.smt2	blob \| history \| raw
-rw-r--r--	250	bug544.smt2	blob \| history \| raw
-rw-r--r--	362	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--	648	bug586.cvc.smt2	blob \| history \| raw
-rw-r--r--	312	bug595.cvc.smt2	blob \| history \| raw
-rw-r--r--	321	bug596.cvc.smt2	blob \| history \| raw
-rw-r--r--	177	bug596b.cvc.smt2	blob \| history \| raw
-rw-r--r--	2566	bug605.cvc.smt2	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
drwxr-xr-x	-	cores	tree \| history
-rw-r--r--	249	cvc-rerror-print.cvc.smt2	blob \| history \| raw
-rw-r--r--	263	cvc3-bug15.cvc.smt2	blob \| history \| raw
-rw-r--r--	887	cvc3.userdoc.01.cvc.smt2	blob \| history \| raw
-rw-r--r--	337	cvc3.userdoc.02.cvc.smt2	blob \| history \| raw
-rw-r--r--	321	cvc3.userdoc.03.cvc.smt2	blob \| history \| raw
-rw-r--r--	394	cvc3.userdoc.04.cvc.smt2	blob \| history \| raw
-rw-r--r--	502	cvc3.userdoc.05.cvc.smt2	blob \| history \| raw
-rw-r--r--	411	cvc3.userdoc.06.cvc.smt2	blob \| history \| raw
-rw-r--r--	673	cvc5-printing.cpp-sample.smt2	blob \| history \| raw
drwxr-xr-x	-	datatypes	tree \| history
drwxr-xr-x	-	decision	tree \| history
-rw-r--r--	196	declare-fun-is-match.smt2	blob \| history \| raw
drwxr-xr-x	-	deep-restart	tree \| history
-rw-r--r--	376	define-fun-model.smt2	blob \| history \| raw
-rw-r--r--	376	difficulty-model-ex.smt2	blob \| history \| raw
-rw-r--r--	300	difficulty-simple.smt2	blob \| history \| raw
-rw-r--r--	257	distinct.smtv1.smt2	blob \| history \| raw
-rw-r--r--	265	dump-unsat-core-full.smt2	blob \| history \| raw
-rw-r--r--	327	echo.smt2	blob \| history \| raw
-rw-r--r--	195	eqrange0.smt2	blob \| history \| raw
-rw-r--r--	608	eqrange1.smt2	blob \| history \| raw
-rw-r--r--	404	eqrange2.smt2	blob \| history \| raw
-rw-r--r--	489	eqrange3.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--	388	get-value-ints.smt2	blob \| history \| raw
-rw-r--r--	268	get-value-no-evaluate.smt2	blob \| history \| raw
-rw-r--r--	860	get-value-reals-ints.smt2	blob \| history \| raw
-rw-r--r--	607	get-value-reals.smt2	blob \| history \| raw
drwxr-xr-x	-	ho	tree \| history
-rw-r--r--	910	hung10_itesdk_output1.smt2	blob \| history \| raw
-rw-r--r--	415	hung13sdk_output1.smt2	blob \| history \| raw
-rw-r--r--	1450	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
drwxr-xr-x	-	int-to-bv	tree \| history
-rw-r--r--	462	issue1063-overloading-dt-cons.smt2	blob \| history \| raw
-rw-r--r--	302	issue1063-overloading-dt-fun.smt2	blob \| history \| raw
-rw-r--r--	296	issue1063-overloading-dt-sel.smt2	blob \| history \| raw
-rw-r--r--	295	issue2832-qualId.smt2	blob \| history \| raw
-rw-r--r--	133	issue4010-sort-inf-var.smt2	blob \| history \| raw
-rw-r--r--	172	issue4469-unc-no-reuse-var.smt2	blob \| history \| raw
-rw-r--r--	655	issue4707-bv-to-bool-small.smt2	blob \| history \| raw
-rw-r--r--	219	issue5099-model-1.smt2	blob \| history \| raw
-rw-r--r--	201	issue5099-model-2.smt2	blob \| history \| raw
-rw-r--r--	90	issue5144-resetAssertions.smt2	blob \| history \| raw
-rw-r--r--	617	issue5187-div-justification.smt2	blob \| history \| raw
-rw-r--r--	566	issue5370.smt2	blob \| history \| raw
-rw-r--r--	1318	issue5462.smt2	blob \| history \| raw
-rw-r--r--	234	issue5473.smt2	blob \| history \| raw
-rw-r--r--	195	issue5540-2-dump-model.smt2	blob \| history \| raw
-rw-r--r--	355	issue5540-model-decls.smt2	blob \| history \| raw
-rw-r--r--	114	issue5550-num-children.smt2	blob \| history \| raw
-rw-r--r--	445	issue5736.smt2	blob \| history \| raw
-rw-r--r--	274	issue5743.smt2	blob \| history \| raw
-rw-r--r--	209	issue5947.smt2	blob \| history \| raw
-rw-r--r--	108	issue6605-2-abd-triv.smt2	blob \| history \| raw
-rw-r--r--	272	issue6738.smt2	blob \| history \| raw
-rw-r--r--	253	issue6741.smt2	blob \| history \| raw
-rw-r--r--	147	issue8807-model-core-partial.smt2	blob \| history \| raw
-rw-r--r--	124	issue8833-interpol-no-shared-var.smt2	blob \| history \| raw
-rw-r--r--	125	issue8834-model-core-nconst.smt2	blob \| history \| raw
-rw-r--r--	180	ite.cvc.smt2	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--	247	lang_opts_2_6_1.smt2	blob \| history \| raw
drwxr-xr-x	-	lemmas	tree \| history
-rw-r--r--	235	let.cvc.smt2	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--	218	logops.01.cvc.smt2	blob \| history \| raw
-rw-r--r--	181	logops.02.cvc.smt2	blob \| history \| raw
-rw-r--r--	214	logops.03.cvc.smt2	blob \| history \| raw
-rw-r--r--	195	logops.04.cvc.smt2	blob \| history \| raw
-rw-r--r--	184	logops.05.cvc.smt2	blob \| history \| raw
-rw-r--r--	450	model-core-non-implied.smt2	blob \| history \| raw
-rw-r--r--	372	model-core.smt2	blob \| history \| raw
-rw-r--r--	254	models-print-1.smt2	blob \| history \| raw
-rw-r--r--	400	models-print-2.smt2	blob \| history \| raw
-rw-r--r--	205	named-expr-use.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--	307	print_define_fun_internal.smt2	blob \| history \| raw
-rw-r--r--	236	print_lambda.cvc.smt2	blob \| history \| raw
-rw-r--r--	366	print_model.cvc.smt2	blob \| history \| raw
drwxr-xr-x	-	printer	tree \| history
-rw-r--r--	151	proj-issue307-get-value-re.smt2	blob \| history \| raw
drwxr-xr-x	-	proofs	tree \| history
drwxr-xr-x	-	push-pop	tree \| history
drwxr-xr-x	-	quantifiers	tree \| history
-rw-r--r--	209	quoted-symbols.smt2	blob \| history \| raw
-rw-r--r--	187	rec-fun-const-parse-bug.smt2	blob \| history \| raw
drwxr-xr-x	-	rels	tree \| history
drwxr-xr-x	-	sep	tree \| history
drwxr-xr-x	-	seq	tree \| history
drwxr-xr-x	-	sets	tree \| history
-rw-r--r--	285	simple-dump-model.smt2	blob \| history \| raw
-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--	291	simple.cvc.smt2	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--	256	smallcnf.cvc.smt2	blob \| history \| raw
-rw-r--r--	375	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--	166	test11.cvc.smt2	blob \| history \| raw
-rw-r--r--	170	test9.cvc.smt2	blob \| history \| raw
drwxr-xr-x	-	tptp	tree \| history
drwxr-xr-x	-	uf	tree \| history
-rw-r--r--	4368	uf20-03.cvc.smt2	blob \| history \| raw
drwxr-xr-x	-	uflia	tree \| history
drwxr-xr-x	-	uflra	tree \| history
drwxr-xr-x	-	unconstrained	tree \| history
drwxr-xr-x	-	use_approx	tree \| history
-rw-r--r--	203	wiki.01.cvc.smt2	blob \| history \| raw
-rw-r--r--	207	wiki.02.cvc.smt2	blob \| history \| raw
-rw-r--r--	189	wiki.03.cvc.smt2	blob \| history \| raw
-rw-r--r--	191	wiki.04.cvc.smt2	blob \| history \| raw
-rw-r--r--	190	wiki.05.cvc.smt2	blob \| history \| raw
-rw-r--r--	190	wiki.06.cvc.smt2	blob \| history \| raw
-rw-r--r--	212	wiki.07.cvc.smt2	blob \| history \| raw
-rw-r--r--	213	wiki.08.cvc.smt2	blob \| history \| raw
-rw-r--r--	182	wiki.09.cvc.smt2	blob \| history \| raw
-rw-r--r--	193	wiki.10.cvc.smt2	blob \| history \| raw
-rw-r--r--	182	wiki.11.cvc.smt2	blob \| history \| raw
-rw-r--r--	183	wiki.12.cvc.smt2	blob \| history \| raw
-rw-r--r--	186	wiki.13.cvc.smt2	blob \| history \| raw
-rw-r--r--	186	wiki.14.cvc.smt2	blob \| history \| raw
-rw-r--r--	188	wiki.15.cvc.smt2	blob \| history \| raw
-rw-r--r--	191	wiki.16.cvc.smt2	blob \| history \| raw
-rw-r--r--	188	wiki.17.cvc.smt2	blob \| history \| raw
-rw-r--r--	188	wiki.18.cvc.smt2	blob \| history \| raw
-rw-r--r--	208	wiki.19.cvc.smt2	blob \| history \| raw
-rw-r--r--	208	wiki.20.cvc.smt2	blob \| history \| raw
-rw-r--r--	187	wiki.21.cvc.smt2	blob \| history \| raw