sets « 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--	abt-min.smt2	394	log plain
-rw-r--r--	abt-te-exh.smt2	302	log plain
-rw-r--r--	abt-te-exh2.smt2	572	log plain
-rw-r--r--	card-2.smt2	276	log plain
-rw-r--r--	card-3sets.cvc.smt2	254	log plain
-rw-r--r--	card.smt2	234	log plain
-rw-r--r--	card3-ground.smt2	141	log plain
-rw-r--r--	comp-qf-error.smt2	320	log plain
-rw-r--r--	complement.cvc.smt2	234	log plain
-rw-r--r--	complement2.cvc.smt2	271	log plain
-rw-r--r--	complement3.cvc.smt2	599	log plain
-rw-r--r--	cvc-sample.cvc.smt2	1712	log plain
-rw-r--r--	dt-simp-mem.smt2	238	log plain
-rw-r--r--	emptyset.smt2	103	log plain
-rw-r--r--	eqtest.smt2	550	log plain
-rw-r--r--	error1.smt2	281	log plain
-rw-r--r--	error2.smt2	112	log plain
-rw-r--r--	insert.smt2	184	log plain
-rw-r--r--	int-real-univ-unsat.smt2	285	log plain
-rw-r--r--	int-real-univ.smt2	285	log plain
d---------	jan24	116	log plain
d---------	jan27	126	log plain
d---------	jan28	72	log plain
d---------	jan30	134	log plain
d---------	mar2014	130	log plain
-rw-r--r--	nonvar-univ.smt2	292	log plain
-rw-r--r--	pre-proc-univ.smt2	249	log plain
-rw-r--r--	rec_copy_loop_check_heap_access_43_4.smt2	5512	log plain
-rw-r--r--	setel-eq.smt2	246	log plain
-rw-r--r--	sets-deq-dd.smt2	230	log plain
-rw-r--r--	sets-equal.smt2	335	log plain
-rw-r--r--	sets-extr.smt2	314	log plain
-rw-r--r--	sets-inter.smt2	287	log plain
-rw-r--r--	sets-new.smt2	390	log plain
-rw-r--r--	sets-of-sets-subtypes.smt2	353	log plain
-rw-r--r--	sets-poly-int-real.smt2	607	log plain
-rw-r--r--	sets-poly-nonint.smt2	301	log plain
-rw-r--r--	sets-sample.smt2	1683	log plain
-rw-r--r--	sets-sharing.smt2	189	log plain
-rw-r--r--	sets-testlemma-ints.smt2	153	log plain
-rw-r--r--	sets-testlemma-reals.smt2	155	log plain
-rw-r--r--	sets-testlemma.smt2	170	log plain
-rw-r--r--	sets-union.smt2	339	log plain
-rw-r--r--	sharing-simp.smt2	340	log plain
-rw-r--r--	union-1a-flip.smt2	336	log plain
-rw-r--r--	union-1a.smt2	336	log plain
-rw-r--r--	union-1b-flip.smt2	336	log plain
-rw-r--r--	union-1b.smt2	336	log plain
-rw-r--r--	union-2.smt2	307	log plain
-rw-r--r--	univset-simp.smt2	544	log plain