sygus « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rwxr-xr-x	General_plus10.sy	277	log plain
-rw-r--r--	aig-si.sy	912	log plain
-rw-r--r--	array-grammar-select.sy	255	log plain
-rw-r--r--	array-grammar-store.sy	360	log plain
-rw-r--r--	c100.sy	393	log plain
-rw-r--r--	ccp16.lus.sy	1096	log plain
-rw-r--r--	cegqi-si-string-triv-2fun.sy	355	log plain
-rw-r--r--	cegqi-si-string-triv.sy	253	log plain
-rw-r--r--	check-generic-red.sy	619	log plain
-rw-r--r--	const-var-test.sy	703	log plain
-rw-r--r--	dt-no-syntax.sy	261	log plain
-rw-r--r--	dt-sel-parse1.sy	1265	log plain
-rw-r--r--	hd-05-d1-prog-nogrammar.sy	234	log plain
-rw-r--r--	inv-different-var-order.sy	500	log plain
-rw-r--r--	issue3356-syg-inf-usort.smt2	253	log plain
-rw-r--r--	issue3624.sy	241	log plain
-rw-r--r--	issue3645-grammar-sets.smt2	169	log plain
-rw-r--r--	issue4383-cache-fv-id.sy	522	log plain
-rw-r--r--	issue4790-dtd.sy	430	log plain
-rw-r--r--	let-ringer.sy	606	log plain
-rw-r--r--	let-simp.sy	401	log plain
-rw-r--r--	no-logic.sy	532	log plain
-rw-r--r--	no-syntax-test-bool.sy	220	log plain
-rw-r--r--	no-syntax-test.sy	214	log plain
-rw-r--r--	pLTL-sygus-syntax-err.sy	2064	log plain
-rw-r--r--	parity-AIG-d0.sy	847	log plain
-rw-r--r--	parse-bv-let.sy	795	log plain
-rw-r--r--	pbe-pred-contra.sy	188	log plain
-rw-r--r--	print-debug.sy	313	log plain
-rw-r--r--	print-define-fun.sy	222	log plain
-rw-r--r--	real-si-all.sy	212	log plain
-rw-r--r--	strings-unconstrained.sy	253	log plain
-rw-r--r--	sygus-no-wf.sy	276	log plain
-rw-r--r--	sygus-uf.sy	556	log plain
-rw-r--r--	uminus_one.sy	208	log plain
-rw-r--r--	univ_3-long-repeat-conflict.sy	2086	log plain