strings « 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--	artemis-0512-nonterm.smt2	394	log plain
-rw-r--r--	at001.smt2	233	log plain
-rw-r--r--	bug615.smt2	756	log plain
-rw-r--r--	bug682.smt2	401	log plain
-rw-r--r--	bug686dd.smt2	329	log plain
-rw-r--r--	bug768.smt2	221	log plain
-rw-r--r--	bug799-min.smt2	393	log plain
-rw-r--r--	chapman150408.smt2	354	log plain
-rw-r--r--	cmu-2db2-extf-reg.smt2	256	log plain
-rw-r--r--	cmu-5042-0707-2.smt2	1155	log plain
-rw-r--r--	cmu-inc-nlpp-071516.smt2	1188	log plain
-rw-r--r--	cmu-substr-rw.smt2	1109	log plain
-rw-r--r--	code-sequence.smt2	398	log plain
-rw-r--r--	complement-test.smt2	401	log plain
-rw-r--r--	crash-1019.smt2	4442	log plain
-rw-r--r--	csp-prefix-exp-bug.smt2	199	log plain
-rw-r--r--	double-replace.smt2	225	log plain
-rw-r--r--	fmf001.smt2	429	log plain
-rw-r--r--	fmf002.smt2	380	log plain
-rw-r--r--	gm-inc-071516-2.smt2	571	log plain
-rw-r--r--	goodAI.smt2	257	log plain
-rw-r--r--	idof-handg.smt2	231	log plain
-rw-r--r--	idof-nconst-index.smt2	276	log plain
-rw-r--r--	idof-neg-index.smt2	204	log plain
-rw-r--r--	idof-triv.smt2	192	log plain
-rw-r--r--	ilc-l-nt.smt2	353	log plain
-rw-r--r--	issue1105.smt2	283	log plain
-rw-r--r--	issue1684-regex.smt2	242	log plain
-rw-r--r--	issue2060.smt2	455	log plain
-rw-r--r--	issue2429-code.smt2	1676	log plain
-rw-r--r--	issue2981.smt2	556	log plain
-rw-r--r--	issue2982.smt2	904	log plain
-rw-r--r--	issue3090.smt2	202	log plain
-rw-r--r--	issue3217.smt2	439	log plain
-rw-r--r--	issue3272.smt2	1401	log plain
-rw-r--r--	issue3357.smt2	694	log plain
-rw-r--r--	issue3657-unexpectedUnsatCVC4.smt2	6601	log plain
-rw-r--r--	issue4379.smt2	287	log plain
-rw-r--r--	kaluza-fl.smt2	6442	log plain
-rw-r--r--	loop002.smt2	178	log plain
-rw-r--r--	loop003.smt2	264	log plain
-rw-r--r--	loop004.smt2	256	log plain
-rw-r--r--	loop005.smt2	380	log plain
-rw-r--r--	loop006.smt2	299	log plain
-rw-r--r--	loop007.smt2	260	log plain
-rw-r--r--	loop008.smt2	187	log plain
-rw-r--r--	loop009.smt2	184	log plain
-rw-r--r--	nf-ff-contains-abs.smt2	460	log plain
-rw-r--r--	no-lazy-pp-quant.smt2	257	log plain
-rw-r--r--	non_termination_regular_expression4.smt2	1237	log plain
-rw-r--r--	norn-13.smt2	728	log plain
-rw-r--r--	norn-360.smt2	1303	log plain
-rw-r--r--	norn-ab.smt2	1056	log plain
-rw-r--r--	norn-nel-bug-052116.smt2	888	log plain
-rw-r--r--	norn-simp-rew-sat.smt2	1013	log plain
-rw-r--r--	nt6-dd.smt2	431	log plain
-rw-r--r--	nterm-re-inter-sigma.smt2	278	log plain
-rw-r--r--	pierre150331.smt2	572	log plain
-rw-r--r--	policy_variable.smt2	1604	log plain
-rw-r--r--	query4674.smt2	737	log plain
-rw-r--r--	query8485.smt2	746	log plain
-rw-r--r--	re-agg-total1.smt2	390	log plain
-rw-r--r--	re-agg-total2.smt2	373	log plain
-rw-r--r--	re-all-char-hard.smt2	610	log plain
-rw-r--r--	re-elim-exact.smt2	265	log plain
-rw-r--r--	re-mod-eq.smt2	532	log plain
-rw-r--r--	re-neg-concat-reduct.smt2	321	log plain
-rw-r--r--	re-neg-unfold-rev-a.smt2	515	log plain
-rw-r--r--	re-unsound-080718.smt2	507	log plain
-rw-r--r--	regexp-strat-fix.smt2	291	log plain
-rw-r--r--	regexp001.smt2	255	log plain
-rw-r--r--	regexp002.smt2	702	log plain
-rw-r--r--	regexp003.smt2	351	log plain
-rw-r--r--	reloop.smt2	531	log plain
-rw-r--r--	repl-empty-sem.smt2	270	log plain
-rw-r--r--	repl-soundness-sem.smt2	308	log plain
-rw-r--r--	replaceall-len.smt2	301	log plain
-rw-r--r--	replaceall-replace.smt2	367	log plain
-rw-r--r--	rev-conv1.smt2	220	log plain
-rw-r--r--	rev-ex1.smt2	238	log plain
-rw-r--r--	rev-ex2.smt2	260	log plain
-rw-r--r--	rev-ex3.smt2	313	log plain
-rw-r--r--	rev-ex4.smt2	324	log plain
-rw-r--r--	rev-ex5.smt2	175	log plain
-rw-r--r--	rew-020618.smt2	387	log plain
-rw-r--r--	rew-check1.smt2	437	log plain
-rw-r--r--	simple-re-consume.smt2	216	log plain
-rw-r--r--	stoi-400million.smt2	168	log plain
-rw-r--r--	stoi-solve.smt2	143	log plain
-rw-r--r--	str-code-sat.smt2	516	log plain
-rw-r--r--	str-code-unsat-2.smt2	190	log plain
-rw-r--r--	str-code-unsat-3.smt2	457	log plain
-rw-r--r--	str-code-unsat.smt2	441	log plain
-rw-r--r--	str-rev-simple-s.smt2	338	log plain
-rw-r--r--	str001.smt2	340	log plain
-rw-r--r--	str002.smt2	410	log plain
-rw-r--r--	str006.smt2	279	log plain
-rw-r--r--	str007.smt2	231	log plain
-rw-r--r--	string-unsound-sem.smt2	467	log plain
-rw-r--r--	strings-index-empty.smt2	366	log plain
-rw-r--r--	strings-leq-trans-unsat.smt2	328	log plain
-rw-r--r--	strings-lt-len5.smt2	206	log plain
-rw-r--r--	strings-lt-simple.smt2	173	log plain
-rw-r--r--	strip-endpt-sound.smt2	649	log plain
-rw-r--r--	substr001.smt2	413	log plain
-rw-r--r--	timeout-no-resp.smt2	233	log plain
-rw-r--r--	tolower-find.smt2	299	log plain
-rw-r--r--	type002.smt2	354	log plain
-rw-r--r--	type003.smt2	254	log plain
-rw-r--r--	username_checker_min.smt2	345	log plain