quantifiers « regress0 « 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--	006-cbqi-ite.smt2	11492	log plain
-rw-r--r--	ARI176e1.smt2	150	log plain
-rw-r--r--	AdditiveMethods_AdditiveMethods..ctor.smt2	45830	log plain
-rw-r--r--	AdditiveMethods_OwnedResults.Mz.smt2	42191	log plain
-rw-r--r--	Arrays_Q1-noinfer.smt2	4185	log plain
-rw-r--r--	Makefile	148	log plain
-rw-r--r--	Makefile.am	2628	log plain
-rw-r--r--	RND-small.smt2	532	log plain
-rw-r--r--	RND_4_16.smt2	4299	log plain
-rw-r--r--	agg-rew-test-cf.smt2	180	log plain
-rw-r--r--	agg-rew-test.smt2	174	log plain
-rwxr-xr-x	anti-sk-simp.smt2	273	log plain
-rw-r--r--	ari056.smt2	94	log plain
-rw-r--r--	array-unsat-simp3.smt2	980	log plain
-rw-r--r--	bi-artm-s.smt2	879	log plain
-rw-r--r--	bignum_quant.smt2	406	log plain
-rw-r--r--	bug269.smt2	490	log plain
-rw-r--r--	bug290.smt2	710	log plain
-rw-r--r--	bug291.smt2	452	log plain
-rw-r--r--	bug291.smt2.expect	56	log plain
-rw-r--r--	burns13.smt2	2612	log plain
-rw-r--r--	burns4.smt2	1412	log plain
-rw-r--r--	cbqi-lia-dt-simp.smt2	236	log plain
-rw-r--r--	cdt-0208-to.smt2	143791	log plain
-rw-r--r--	clock-10.smt2	161	log plain
-rw-r--r--	clock-3.smt2	160	log plain
-rw-r--r--	delta-simp.smt2	132	log plain
-rw-r--r--	double-pattern.smt2	179	log plain
-rw-r--r--	ex3.smt2	258	log plain
-rw-r--r--	ex6.smt2	349	log plain
-rw-r--r--	ext-ex-deq-trigger.smt2	667	log plain
-rw-r--r--	floor.smt2	138	log plain
-rw-r--r--	florian-case-ax.smt2	6650	log plain
-rw-r--r--	gauss_init_0030.fof.smt2	7666	log plain
-rw-r--r--	inst-max-level-segf.smt2	14232	log plain
-rw-r--r--	is-even-pred.smt2	225	log plain
-rw-r--r--	is-even.smt2	260	log plain
-rw-r--r--	is-int.smt2	263	log plain
-rw-r--r--	javafe.ast.ArrayInit.35.smt2	95882	log plain
-rw-r--r--	javafe.ast.StandardPrettyPrint.319.smt2	134345	log plain
-rw-r--r--	javafe.ast.StmtVec.009.smt2	31334	log plain
-rw-r--r--	javafe.ast.WhileStmt.447.smt2	93917	log plain
-rw-r--r--	javafe.tc.CheckCompilationUnit.001.smt2	75099	log plain
-rw-r--r--	javafe.tc.FlowInsensitiveChecks.682.smt2	160472	log plain
-rw-r--r--	macro-subtype-param.smt2	500	log plain
-rw-r--r--	macros-int-real.smt2	198	log plain
-rw-r--r--	macros-real-arg.smt2	301	log plain
-rw-r--r--	matching-lia-1arg.smt2	178	log plain
-rw-r--r--	mix-coeff.smt2	209	log plain
-rw-r--r--	mix-match.smt2	191	log plain
-rw-r--r--	mix-simp.smt2	138	log plain
-rw-r--r--	nested-delta.smt2	180	log plain
-rw-r--r--	nested-inf.smt2	152	log plain
-rw-r--r--	opisavailable-12.smt2	15872	log plain
-rw-r--r--	parametric-lists.smt2	1172	log plain
-rw-r--r--	partial-trigger.smt2	232	log plain
-rw-r--r--	psyco-196.smt2	15383	log plain
-rw-r--r--	pure_dt_cbqi.smt2	193	log plain
-rw-r--r--	qcf-rel-dom-opt.smt2	822	log plain
-rw-r--r--	qcft-javafe.filespace.TreeWalker.006.smt2	37428	log plain
-rw-r--r--	qcft-smtlib3dbc51.smt2	78822	log plain
-rw-r--r--	refcount24.cvc	6720	log plain
-rw-r--r--	rew-to-0211-dd.smt2	19565	log plain
-rw-r--r--	rew-to-scala.smt2	2804	log plain
-rw-r--r--	ricart-agrawala6.smt2	3989	log plain
-rw-r--r--	set3.smt2	1385	log plain
-rw-r--r--	set8.smt2	1445	log plain
-rw-r--r--	simp-len.smt2	241	log plain
-rw-r--r--	simp-typ-test.smt2	185	log plain
-rw-r--r--	smtlib384a03.smt2	43696	log plain
-rw-r--r--	smtlib46f14a.smt2	43323	log plain
-rw-r--r--	smtlibf957ea.smt2	43937	log plain
-rw-r--r--	stream-x2014-09-18-unsat.smt2	17620	log plain
-rw-r--r--	subtype-param-unk.smt2	496	log plain
-rw-r--r--	subtype-param.smt2	405	log plain
-rw-r--r--	symmetric_unsat_7.smt2	1534	log plain