sygus « regress1 « 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--	Base16_1.sy	994	log plain
-rw-r--r--	VC22_a.sy	1458	log plain
-rw-r--r--	abv.sy	1193	log plain
-rw-r--r--	array_search_2.sy	568	log plain
-rw-r--r--	array_search_5-Q-easy.sy	2805	log plain
-rw-r--r--	array_sum_2_5.sy	465	log plain
-rw-r--r--	bvudiv-by-2.sy	648	log plain
-rwxr-xr-x	car_3.lus.sy	13182	log plain
-rw-r--r--	cegar1.sy	512	log plain
-rw-r--r--	cegis-unif-inv-eq-fair.sy	12654	log plain
-rw-r--r--	cegisunif-depth1.sy	628	log plain
-rw-r--r--	cggmp.sy	502	log plain
-rw-r--r--	clock-inc-tuple.sy	531	log plain
-rw-r--r--	commutative-stream.sy	567	log plain
-rw-r--r--	commutative.sy	372	log plain
-rw-r--r--	constant-bool-si-all.sy	248	log plain
-rw-r--r--	constant-dec-tree-bug.sy	277	log plain
-rw-r--r--	constant-ite-bv.sy	1057	log plain
-rw-r--r--	constant.sy	397	log plain
-rw-r--r--	crci-ssb-unk.sy	1118	log plain
-rw-r--r--	crcy-si-rcons.sy	2823	log plain
-rw-r--r--	crcy-si.sy	491	log plain
-rw-r--r--	dt-test-ns.sy	331	log plain
-rw-r--r--	dup-op.sy	249	log plain
-rw-r--r--	enum-test.sy	336	log plain
-rw-r--r--	fg_polynomial3.sy	281	log plain
-rw-r--r--	find_sc_bvult_bvnot.sy	1558	log plain
-rw-r--r--	hd-01-d1-prog.sy	578	log plain
-rw-r--r--	hd-19-d1-prog-dup-op.sy	822	log plain
-rw-r--r--	hd-sdiv.sy	424	log plain
-rw-r--r--	icfp_14.12-flip-args.sy	2514	log plain
-rw-r--r--	icfp_14.12.sy	2986	log plain
-rw-r--r--	icfp_14_12_diff_types.sy	1299	log plain
-rw-r--r--	icfp_28_10.sy	1470	log plain
-rw-r--r--	icfp_easy-ite.sy	1094	log plain
-rw-r--r--	inv-example.sy	569	log plain
-rw-r--r--	inv-missed-sol-true.sy	612	log plain
-rw-r--r--	inv-unused.sy	532	log plain
-rw-r--r--	inv_gen_fig8.sy	1733	log plain
-rw-r--r--	large-const-simp.sy	254	log plain
-rw-r--r--	let-bug-simp.sy	365	log plain
-rw-r--r--	list-head-x.sy	297	log plain
-rw-r--r--	logiccell_help.sy	3153	log plain
-rw-r--r--	max.sy	943	log plain
-rw-r--r--	max2-bv.sy	334	log plain
-rw-r--r--	multi-fun-polynomial2.sy	618	log plain
-rw-r--r--	nflat-fwd-3.sy	219	log plain
-rw-r--r--	nflat-fwd.sy	241	log plain
-rw-r--r--	nia-max-square-ns.sy	267	log plain
-rw-r--r--	no-flat-simp.sy	333	log plain
-rw-r--r--	no-mention.sy	254	log plain
-rw-r--r--	parity-si-rcons.sy	1110	log plain
-rw-r--r--	pbe_multi.sy	2467	log plain
-rw-r--r--	phone-1-long.sy	5160	log plain
-rw-r--r--	planning-unif.sy	9285	log plain
-rw-r--r--	process-10-vars.sy	593	log plain
-rw-r--r--	qe.sy	238	log plain
-rw-r--r--	real-grammar.sy	267	log plain
-rw-r--r--	simple-regexp.sy	732	log plain
-rw-r--r--	stopwatch-bt.sy	5573	log plain
-rw-r--r--	strings-concat-3-args.sy	428	log plain
-rw-r--r--	strings-double-rec.sy	354	log plain
-rw-r--r--	strings-small.sy	572	log plain
-rw-r--r--	strings-template-infer-unused.sy	382	log plain
-rw-r--r--	strings-template-infer.sy	348	log plain
-rw-r--r--	strings-trivial-simp.sy	287	log plain
-rw-r--r--	strings-trivial-two-type.sy	412	log plain
-rw-r--r--	strings-trivial.sy	326	log plain
-rw-r--r--	sygus-dt.sy	499	log plain
-rw-r--r--	sygus-lambda-fv.sy	499	log plain
-rw-r--r--	sygus-uf-ex.sy	426	log plain
-rw-r--r--	t8.sy	790	log plain
-rw-r--r--	tl-type-0.sy	228	log plain
-rw-r--r--	tl-type-4x.sy	241	log plain
-rw-r--r--	tl-type.sy	241	log plain
-rw-r--r--	triv-type-mismatch-si.sy	188	log plain
-rw-r--r--	trivial-stream.sy	448	log plain
-rw-r--r--	twolets1.sy	710	log plain
-rw-r--r--	twolets2-orig.sy	600	log plain
-rw-r--r--	unbdd_inv_gen_ex7.sy	1707	log plain
-rw-r--r--	unbdd_inv_gen_winf1.sy	1402	log plain
-rw-r--r--	univ_2-long-repeat.sy	4720	log plain