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--	ARI176e1.smt2	150	log plain
-rw-r--r--	agg-rew-test-cf.smt2	180	log plain
-rw-r--r--	agg-rew-test.smt2	174	log plain
-rw-r--r--	ari056.smt2	133	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--	bug749-rounding.smt2	283	log plain
-rw-r--r--	cbqi-lia-dt-simp.smt2	257	log plain
-rw-r--r--	cegqi-nl-simp.cvc	66	log plain
-rw-r--r--	cegqi-nl-sq.smt2	112	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	181	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--	floor.smt2	138	log plain
-rw-r--r--	horn-ground-pre-post.smt2	284	log plain
-rw-r--r--	is-even-pred.smt2	225	log plain
-rw-r--r--	is-int.smt2	263	log plain
-rw-r--r--	issue1805.smt2	233	log plain
-rw-r--r--	issue2031-bv-var-elim.smt2	336	log plain
-rw-r--r--	issue2033-macro-arith.smt2	282	log plain
-rw-r--r--	lra-triv-gn.smt2	206	log plain
-rw-r--r--	macros-int-real.smt2	198	log plain
-rw-r--r--	macros-real-arg.smt2	310	log plain
-rw-r--r--	matching-lia-1arg.smt2	178	log plain
-rw-r--r--	mix-complete-strat.smt2	338	log plain
-rw-r--r--	mix-match.smt2	191	log plain
-rw-r--r--	mix-simp.smt2	177	log plain
-rw-r--r--	nested-delta.smt2	180	log plain
-rw-r--r--	nested-inf.smt2	152	log plain
-rw-r--r--	partial-trigger.smt2	232	log plain
-rw-r--r--	pure_dt_cbqi.smt2	246	log plain
-rw-r--r--	qbv-inequality2.smt2	247	log plain
-rw-r--r--	qbv-multi-lit-uge.smt2	281	log plain
-rw-r--r--	qbv-simp.smt2	261	log plain
-rw-r--r--	qbv-test-invert-bvadd-neq.smt2	250	log plain
-rw-r--r--	qbv-test-invert-bvand-neq.smt2	246	log plain
-rw-r--r--	qbv-test-invert-bvand.smt2	252	log plain
-rw-r--r--	qbv-test-invert-bvashr-0-neq.smt2	251	log plain
-rw-r--r--	qbv-test-invert-bvashr-1-neq.smt2	247	log plain
-rw-r--r--	qbv-test-invert-bvlshr-0-neq.smt2	251	log plain
-rw-r--r--	qbv-test-invert-bvlshr-0.smt2	253	log plain
-rw-r--r--	qbv-test-invert-bvlshr-1-neq.smt2	247	log plain
-rw-r--r--	qbv-test-invert-bvor-neq.smt2	245	log plain
-rw-r--r--	qbv-test-invert-bvor.smt2	251	log plain
-rw-r--r--	qbv-test-invert-bvshl-0-neq.smt2	246	log plain
-rw-r--r--	qbv-test-invert-bvshl-0.smt2	252	log plain
-rw-r--r--	qbv-test-invert-bvult-1.smt2	214	log plain
-rw-r--r--	qbv-test-invert-bvxor-neq.smt2	234	log plain
-rw-r--r--	qbv-test-invert-bvxor.smt2	232	log plain
-rw-r--r--	qbv-test-invert-concat-0-neq.smt2	252	log plain
-rw-r--r--	qbv-test-invert-concat-0.smt2	254	log plain
-rw-r--r--	qbv-test-invert-concat-1-neq.smt2	252	log plain
-rw-r--r--	qbv-test-invert-concat-1.smt2	254	log plain
-rw-r--r--	qbv-test-invert-sign-extend.smt2	263	log plain
-rw-r--r--	qcf-rel-dom-opt.smt2	822	log plain
-rw-r--r--	rew-to-scala.smt2	2850	log plain
-rw-r--r--	simp-len.smt2	245	log plain
-rw-r--r--	simp-typ-test.smt2	185	log plain