rewriterules « 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--	datatypes2.smt2	5760	log plain
-rw-r--r--	datatypes3.smt2	4863	log plain
-rw-r--r--	datatypes_clark_quantification.smt2	8749	log plain
-rw-r--r--	datatypes_sat.smt2	3299	log plain
-rw-r--r--	length_gen.smt2	885	log plain
-rw-r--r--	length_gen_010.smt2	931	log plain
-rw-r--r--	length_gen_010_lemma.smt2	831	log plain
-rw-r--r--	length_gen_020.smt2	885	log plain
-rw-r--r--	length_gen_020_sat.smt2	884	log plain
-rw-r--r--	length_gen_040.smt2	885	log plain
-rw-r--r--	length_gen_040_lemma.smt2	831	log plain
-rw-r--r--	length_gen_040_lemma_trigger.smt2	943	log plain
-rw-r--r--	length_gen_080.smt2	885	log plain
-rw-r--r--	length_gen_160_lemma.smt2	833	log plain
-rw-r--r--	length_gen_inv_160.smt2	887	log plain
-rw-r--r--	length_trick3.smt2	995	log plain
-rw-r--r--	length_trick3_int.smt2	1262	log plain
-rw-r--r--	reachability_back_to_the_future.smt2	1951	log plain
-rw-r--r--	read5.smt2	2497	log plain
-rw-r--r--	set_A_new_fast_tableau-base.smt2	4704	log plain
-rw-r--r--	set_A_new_fast_tableau-base_sat.smt2	4608	log plain
-rw-r--r--	test_guards.smt2	1180	log plain
-rw-r--r--	why3_vstte10_max_sum_harness2.smt2	15726	log plain