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	128	log plain
-rw-r--r--	agg-rew-test-cf.smt2	230	log plain
-rw-r--r--	agg-rew-test.smt2	224	log plain
-rw-r--r--	ari056.smt2	134	log plain
-rw-r--r--	bug269.smt2	490	log plain
-rw-r--r--	bug290.smt2	710	log plain
-rw-r--r--	bug291.smt2	509	log plain
-rw-r--r--	bug749-rounding.smt2	283	log plain
-rw-r--r--	cbqi-lia-dt-simp.smt2	247	log plain
-rw-r--r--	cegqi-needs-justify.smt2	290	log plain
-rw-r--r--	cegqi-nl-simp.cvc	99	log plain
-rw-r--r--	cegqi-nl-sq.smt2	112	log plain
-rw-r--r--	cegqi-par-dt-simple.smt2	204	log plain
-rw-r--r--	clock-10.smt2	161	log plain
-rw-r--r--	clock-3.smt2	160	log plain
-rw-r--r--	cond-var-elim-binary.smt2	355	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--	issue2035.smt2	1170	log plain
-rw-r--r--	issue3655.smt2	419	log plain
-rw-r--r--	issue4086-infs.smt2	249	log plain
-rw-r--r--	issue4275-qcf-cegqi-rep.smt2	266	log plain
-rw-r--r--	issue4437-unc-quant.smt2	305	log plain
-rw-r--r--	issue4576.smt2	194	log plain
-rw-r--r--	issue5645-dt-cm-spurious.smt2	160	log plain
-rw-r--r--	issue5693-prenex.smt2	273	log plain
-rw-r--r--	lra-triv-gn.smt2	188	log plain
-rw-r--r--	macros-int-real.smt2	198	log plain
-rw-r--r--	macros-real-arg.smt2	368	log plain
-rw-r--r--	matching-lia-1arg.smt2	178	log plain
-rw-r--r--	mix-complete-strat.smt2	339	log plain
-rw-r--r--	mix-match.smt2	247	log plain
-rw-r--r--	mix-simp.smt2	177	log plain
-rw-r--r--	nested-delta.smt2	136	log plain
-rw-r--r--	nested-inf.smt2	108	log plain
-rw-r--r--	partial-trigger.smt2	232	log plain
-rw-r--r--	pure_dt_cbqi.smt2	247	log plain
-rw-r--r--	qarray-sel-over-store.smt2	817	log plain
-rw-r--r--	qbv-inequality2.smt2	249	log plain
-rw-r--r--	qbv-multi-lit-uge.smt2	267	log plain
-rw-r--r--	qbv-simp.smt2	263	log plain
-rw-r--r--	qbv-test-invert-bvadd-neq.smt2	253	log plain
-rw-r--r--	qbv-test-invert-bvand-neq.smt2	249	log plain
-rw-r--r--	qbv-test-invert-bvand.smt2	255	log plain
-rw-r--r--	qbv-test-invert-bvashr-0-neq.smt2	254	log plain
-rw-r--r--	qbv-test-invert-bvashr-1-neq.smt2	250	log plain
-rw-r--r--	qbv-test-invert-bvlshr-0-neq.smt2	250	log plain
-rw-r--r--	qbv-test-invert-bvlshr-0.smt2	256	log plain
-rw-r--r--	qbv-test-invert-bvlshr-1-neq.smt2	250	log plain
-rw-r--r--	qbv-test-invert-bvor-neq.smt2	248	log plain
-rw-r--r--	qbv-test-invert-bvor.smt2	254	log plain
-rw-r--r--	qbv-test-invert-bvshl-0-neq.smt2	249	log plain
-rw-r--r--	qbv-test-invert-bvshl-0.smt2	255	log plain
-rw-r--r--	qbv-test-invert-bvult-1.smt2	217	log plain
-rw-r--r--	qbv-test-invert-bvxor-neq.smt2	237	log plain
-rw-r--r--	qbv-test-invert-bvxor.smt2	212	log plain
-rw-r--r--	qbv-test-invert-concat-0-neq.smt2	255	log plain
-rw-r--r--	qbv-test-invert-concat-0.smt2	257	log plain
-rw-r--r--	qbv-test-invert-concat-1-neq.smt2	255	log plain
-rw-r--r--	qbv-test-invert-concat-1.smt2	257	log plain
-rw-r--r--	qbv-test-invert-sign-extend.smt2	266	log plain
-rw-r--r--	qcf-rel-dom-opt.smt2	822	log plain
-rw-r--r--	quant-model-simplification.smt2	218	log plain
-rw-r--r--	rew-to-scala.smt2	2946	log plain
-rw-r--r--	selector-trigger.smt2	240	log plain
-rw-r--r--	simp-len.smt2	249	log plain
-rw-r--r--	simp-typ-test.smt2	185	log plain
-rw-r--r--	ufnia-fv-delta.smt2	205	log plain