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	1075	log plain
-rw-r--r--	VC22_a.sy	1516	log plain
-rw-r--r--	abd-simple-conj-4.smt2	356	log plain
-rw-r--r--	abduction_1255.corecstrs.readable.smt2	2317	log plain
-rw-r--r--	abduction_streq.readable.smt2	1400	log plain
-rw-r--r--	abv.sy	1460	log plain
-rw-r--r--	array-grammar-store.sy	360	log plain
-rw-r--r--	array_search_2.sy	611	log plain
-rw-r--r--	array_search_5-Q-easy.sy	2881	log plain
-rw-r--r--	array_sum_2_5.sy	509	log plain
-rw-r--r--	bvudiv-by-2.sy	710	log plain
-rwxr-xr-x	car_3.lus.sy	13151	log plain
-rw-r--r--	cegar1.sy	469	log plain
-rw-r--r--	cegis-unif-inv-eq-fair.sy	11889	log plain
-rw-r--r--	cggmp.sy	459	log plain
-rw-r--r--	clock-inc-tuple.sy	533	log plain
-rw-r--r--	coeff-solve-inv.sy	516	log plain
-rw-r--r--	commutative-stream.sy	623	log plain
-rw-r--r--	commutative.sy	404	log plain
-rw-r--r--	complex-no-rewrite.sy	519	log plain
-rw-r--r--	complex-rewrite-in-db.sy	519	log plain
-rw-r--r--	concat_extract_example.sy	644	log plain
-rw-r--r--	constant-bool-si-all.sy	262	log plain
-rw-r--r--	constant-dec-tree-bug.sy	303	log plain
-rw-r--r--	constant-ite-bv.sy	1120	log plain
-rw-r--r--	constant.sy	429	log plain
-rw-r--r--	crci-ssb-unk.sy	1213	log plain
-rw-r--r--	crcy-si-rcons.sy	2985	log plain
-rw-r--r--	crcy-si.sy	541	log plain
-rw-r--r--	cube-nia.sy	409	log plain
-rw-r--r--	double.sy	410	log plain
-rw-r--r--	dt-test-ns.sy	350	log plain
-rw-r--r--	dup-op.sy	290	log plain
-rw-r--r--	eq-sub-obs.sy	848	log plain
-rw-r--r--	error1-dt.sy	1862	log plain
-rw-r--r--	eval-uc.sy	929	log plain
-rw-r--r--	extract.sy	349	log plain
-rw-r--r--	fast-enum-backtrack.sy	599	log plain
-rw-r--r--	fg_polynomial3.sy	292	log plain
-rw-r--r--	find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy	509	log plain
-rw-r--r--	find_sc_bvult_bvnot.sy	1663	log plain
-rw-r--r--	ground-ite-free-constant-si.sy	793	log plain
-rw-r--r--	hd-01-d1-prog.sy	556	log plain
-rw-r--r--	hd-19-d1-prog-dup-op.sy	882	log plain
-rw-r--r--	hd-sdiv.sy	483	log plain
-rw-r--r--	ho-sygus.sy	239	log plain
-rw-r--r--	icfp_14.12-flip-args.sy	2617	log plain
-rw-r--r--	icfp_14.12.sy	3089	log plain
-rw-r--r--	icfp_14_12_diff_types.sy	1428	log plain
-rw-r--r--	icfp_28_10.sy	1522	log plain
-rw-r--r--	icfp_easy-ite.sy	1217	log plain
-rw-r--r--	int-any-const.sy	426	log plain
-rw-r--r--	interpol1.smt2	506	log plain
-rw-r--r--	interpol3.smt2	193	log plain
-rw-r--r--	interpol_arr1.smt2	324	log plain
-rw-r--r--	interpol_arr2.smt2	584	log plain
-rw-r--r--	interpol_cosa_1.smt2	3084	log plain
-rw-r--r--	interpol_dt.smt2	360	log plain
-rw-r--r--	interpol_from_pono_1.smt2	4908	log plain
-rw-r--r--	interpol_from_pono_2.smt2	8314	log plain
-rw-r--r--	interpol_from_pono_3.smt2	15110	log plain
-rw-r--r--	inv-example.sy	501	log plain
-rw-r--r--	inv-missed-sol-true.sy	572	log plain
-rw-r--r--	inv-unused.sy	464	log plain
-rw-r--r--	inv_gen_fig8.sy	1813	log plain
-rw-r--r--	issue2914.sy	548	log plain
-rw-r--r--	issue2935.sy	843	log plain
-rw-r--r--	issue3199.smt2	127	log plain
-rw-r--r--	issue3200.smt2	130	log plain
-rw-r--r--	issue3201.smt2	138	log plain
-rw-r--r--	issue3205.smt2	131	log plain
-rw-r--r--	issue3247.smt2	466	log plain
-rw-r--r--	issue3320-quant.sy	286	log plain
-rw-r--r--	issue3461.sy	370	log plain
-rw-r--r--	issue3498.smt2	141	log plain
-rw-r--r--	issue3507.smt2	216	log plain
-rw-r--r--	issue3514.smt2	263	log plain
-rw-r--r--	issue3580.sy	427	log plain
-rw-r--r--	issue3633.smt2	130	log plain
-rw-r--r--	issue3634.smt2	159	log plain
-rw-r--r--	issue3635.smt2	163	log plain
-rw-r--r--	issue3644.smt2	153	log plain
-rw-r--r--	issue3648.smt2	194	log plain
-rw-r--r--	issue3649.sy	686	log plain
-rw-r--r--	issue3802-default-consts.sy	337	log plain
-rw-r--r--	issue3839-cond-rewrite.smt2	247	log plain
-rw-r--r--	issue3944-div-rewrite.smt2	237	log plain
-rw-r--r--	issue3947-agg-miniscope.smt2	247	log plain
-rw-r--r--	issue3995-fmf-var-op.smt2	164	log plain
-rw-r--r--	issue4009-qep.smt2	226	log plain
-rw-r--r--	issue4025-no-rlv-cond.smt2	254	log plain
-rw-r--r--	issue4083-var-shadow.smt2	308	log plain
-rw-r--r--	issue5848-3-trivial-no-abduct.smt2	114	log plain
-rw-r--r--	large-const-simp.sy	268	log plain
-rw-r--r--	let-bug-simp.sy	526	log plain
-rw-r--r--	list-head-x.sy	305	log plain
-rw-r--r--	list_recursor.sy	762	log plain
-rw-r--r--	logiccell_help.sy	3455	log plain
-rw-r--r--	max.sy	1024	log plain
-rw-r--r--	max2-bv.sy	361	log plain
-rw-r--r--	multi-fun-polynomial2.sy	700	log plain
-rw-r--r--	nflat-fwd-3.sy	260	log plain
-rw-r--r--	nflat-fwd.sy	282	log plain
-rw-r--r--	nia-max-square-ns.sy	281	log plain
-rw-r--r--	no-flat-simp.sy	363	log plain
-rw-r--r--	no-mention.sy	267	log plain
-rw-r--r--	no-var-in-sol.sy	708	log plain
-rw-r--r--	node-discrete.sy	5383	log plain
-rw-r--r--	once_2.sy	818	log plain
-rw-r--r--	only-const-grammar.sy	327	log plain
-rw-r--r--	pLTL_5_trace.sy	11046	log plain
-rw-r--r--	parity-si-rcons.sy	1166	log plain
-rw-r--r--	pbe_multi.sy	2631	log plain
-rw-r--r--	phone-1-long.sy	4984	log plain
-rw-r--r--	planning-unif.sy	9428	log plain
-rw-r--r--	process-10-vars.sy	607	log plain
-rw-r--r--	qe.sy	252	log plain
-rw-r--r--	qf_abv.smt2	2853	log plain
-rw-r--r--	re-concat.sy	431	log plain
-rw-r--r--	real-any-const.sy	311	log plain
-rw-r--r--	real-grammar.sy	281	log plain
-rw-r--r--	rec-fun-swap.sy	1623	log plain
-rw-r--r--	rec-fun-sygus.sy	733	log plain
-rw-r--r--	rec-fun-while-1.sy	2040	log plain
-rw-r--r--	rec-fun-while-2.sy	2092	log plain
-rw-r--r--	rec-fun-while-infinite.sy	2141	log plain
-rw-r--r--	repair-const-rl.sy	495	log plain
-rw-r--r--	replicate-mod.sy	10684	log plain
-rw-r--r--	rex-strings-alarm.sy	965	log plain
-rw-r--r--	sets-pred-test.sy	385	log plain
-rw-r--r--	simple-no-rewrite.sy	303	log plain
-rw-r--r--	simple-not-in-grammar.sy	188	log plain
-rw-r--r--	simple-regexp.sy	898	log plain
-rw-r--r--	simple-rewrite-in-db.sy	296	log plain
-rw-r--r--	simple-rewrite-not-in-db.sy	374	log plain
-rw-r--r--	stopwatch-bt.sy	5208	log plain
-rw-r--r--	strings-any-term1.sy	355	log plain
-rw-r--r--	strings-concat-3-args.sy	458	log plain
-rw-r--r--	strings-double-rec.sy	418	log plain
-rw-r--r--	strings-no-syntax.sy	286	log plain
-rw-r--r--	strings-small.sy	600	log plain
-rw-r--r--	strings-template-infer-unused.sy	414	log plain
-rw-r--r--	strings-template-infer.sy	380	log plain
-rw-r--r--	strings-trivial-simp.sy	320	log plain
-rw-r--r--	strings-trivial-two-type.sy	393	log plain
-rw-r--r--	strings-trivial.sy	331	log plain
-rw-r--r--	sygus-dt.sy	525	log plain
-rw-r--r--	sygus-lambda-fv.sy	564	log plain
-rw-r--r--	sygus-uf-ex.sy	498	log plain
-rw-r--r--	t8.sy	841	log plain
-rw-r--r--	temp_input_to_synth_ic-error-121418.sy	656	log plain
-rw-r--r--	tester.sy	639	log plain
-rw-r--r--	tl-type-0.sy	270	log plain
-rw-r--r--	tl-type-4x.sy	283	log plain
-rw-r--r--	tl-type.sy	283	log plain
-rw-r--r--	triv-type-mismatch-si.sy	201	log plain
-rw-r--r--	trivial-stream.sy	474	log plain
-rw-r--r--	twolets1.sy	805	log plain
-rw-r--r--	twolets2-orig.sy	676	log plain
-rw-r--r--	uf-abduct.smt2	265	log plain
-rw-r--r--	unbdd_inv_gen_winf1.sy	1513	log plain
-rw-r--r--	univ_2-long-repeat.sy	4631	log plain
-rw-r--r--	yoni-true-sol.smt2	419	log plain