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	237	log plain
-rw-r--r--	aig-si.sy	870	log plain
-rw-r--r--	array-grammar-select.sy	241	log plain
-rw-r--r--	array-grammar-store.sy	332	log plain
-rw-r--r--	c100.sy	362	log plain
-rw-r--r--	ccp16.lus.sy	1164	log plain
-rw-r--r--	cegqi-si-string-triv-2fun.sy	341	log plain
-rw-r--r--	cegqi-si-string-triv.sy	239	log plain
-rw-r--r--	check-generic-red.sy	557	log plain
-rw-r--r--	const-var-test.sy	656	log plain
-rw-r--r--	dt-no-syntax.sy	247	log plain
-rw-r--r--	dt-sel-parse1.sy	1171	log plain
-rw-r--r--	hd-05-d1-prog-nogrammar.sy	214	log plain
-rw-r--r--	inv-different-var-order.sy	567	log plain
-rw-r--r--	let-ringer.sy	548	log plain
-rw-r--r--	let-simp.sy	370	log plain
-rw-r--r--	no-syntax-test-bool.sy	207	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--	real-si-all.sy	198	log plain
-rw-r--r--	strings-unconstrained.sy	247	log plain
-rw-r--r--	sygus-uf.sy	449	log plain
-rw-r--r--	uminus_one.sy	180	log plain
-rw-r--r--	univ_3-long-repeat-conflict.sy	2052	log plain