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	1404	log plain
-rw-r--r--	array_search_2.sy	568	log plain
-rw-r--r--	array_sum_2_5.sy	465	log plain
-rw-r--r--	cegar1.sy	512	log plain
-rw-r--r--	cggmp.sy	502	log plain
-rw-r--r--	clock-inc-tuple.sy	506	log plain
-rw-r--r--	commutative.sy	372	log plain
-rw-r--r--	constant-ite-bv.sy	1057	log plain
-rw-r--r--	constant.sy	397	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	241	log plain
-rw-r--r--	fg_polynomial3.sy	281	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_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-unused.sy	532	log plain
-rw-r--r--	inv_gen_fig8.sy	1733	log plain
-rw-r--r--	list-head-x.sy	297	log plain
-rw-r--r--	max.sy	943	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--	pbe_multi.sy	2467	log plain
-rw-r--r--	process-10-vars.sy	572	log plain
-rw-r--r--	qe.sy	238	log plain
-rw-r--r--	real-grammar.sy	267	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	474	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--	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