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	391	log plain
-rw-r--r--	at001.smt2	230	log plain
-rw-r--r--	bug615.smt2	756	log plain
-rw-r--r--	bug682.smt2	401	log plain
-rw-r--r--	bug686dd.smt2	321	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--	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	377	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	1673	log plain
-rw-r--r--	kaluza-fl.smt2	6439	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	377	log plain
-rw-r--r--	loop006.smt2	299	log plain
-rw-r--r--	loop007.smt2	257	log plain
-rw-r--r--	loop008.smt2	184	log plain
-rw-r--r--	loop009.smt2	184	log plain
-rw-r--r--	nf-ff-contains-abs.smt2	460	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--	nterm-re-inter-sigma.smt2	278	log plain
-rw-r--r--	pierre150331.smt2	564	log plain
-rw-r--r--	policy_variable.smt2	1604	log plain
-rw-r--r--	re-elim-exact.smt2	265	log plain
-rw-r--r--	re-unsound-080718.smt2	507	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	511	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--	rew-020618.smt2	387	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--	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	410	log plain
-rw-r--r--	type002.smt2	351	log plain
-rw-r--r--	type003.smt2	251	log plain
-rw-r--r--	username_checker_min.smt2	345	log plain