sygus « regress0 « 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
-rwxr-xr-x	General_plus10.sy	237	log plain
-rw-r--r--	Makefile	142	log plain
-rw-r--r--	Makefile.am	2792	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--	c100.sy	362	log plain
-rw-r--r--	ccp16.lus.sy	1164	log plain
-rw-r--r--	cegar1.sy	512	log plain
-rw-r--r--	cggmp.sy	502	log plain
-rw-r--r--	check-generic-red.sy	532	log plain
-rw-r--r--	clock-inc-tuple.sy	506	log plain
-rw-r--r--	commutative.sy	372	log plain
-rw-r--r--	const-var-test.sy	656	log plain
-rw-r--r--	constant.sy	397	log plain
-rw-r--r--	dt-no-syntax.sy	247	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--	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--	let-ringer.sy	441	log plain
-rw-r--r--	let-simp.sy	347	log plain
-rw-r--r--	list-head-x.sy	297	log plain
-rw-r--r--	max.smt2	3765	log plain
-rw-r--r--	max.sy	943	log plain
-rw-r--r--	max2-univ.sy	399	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--	no-syntax-test-bool.sy	207	log plain
-rw-r--r--	no-syntax-test-no-si.sy	212	log plain
-rw-r--r--	no-syntax-test.sy	201	log plain
-rw-r--r--	parity-AIG-d0.sy	807	log plain
-rw-r--r--	parse-bv-let.sy	739	log plain
-rw-r--r--	process-10-vars-2fun.sy	801	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-neg.sy	256	log plain
-rw-r--r--	real-si-all.sy	198	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--	strings-unconstrained.sy	247	log plain
-rw-r--r--	sygus-dt.sy	474	log plain
-rw-r--r--	sygus-uf.sl	449	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--	uminus_one.sy	180	log plain
-rw-r--r--	unbdd_inv_gen_winf1.sy	1402	log plain