arrays « 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--	arrays0.smt2	660	log plain
-rw-r--r--	arrays1.smt2	741	log plain
-rw-r--r--	arrays2.smt2	763	log plain
-rw-r--r--	arrays3.smt2	772	log plain
-rw-r--r--	arrays4.smt2	774	log plain
-rw-r--r--	bool-array.smt2	257	log plain
-rw-r--r--	bug272.minimized.smtv1.smt2	765	log plain
-rw-r--r--	bug272.smtv1.smt2	12191	log plain
-rw-r--r--	bug3020.smt2	412	log plain
-rw-r--r--	bug4957.smt2	171	log plain
-rw-r--r--	bug637.delta.smt2	363	log plain
-rw-r--r--	constarr.cvc	140	log plain
-rw-r--r--	constarr.smt2	241	log plain
-rw-r--r--	constarr2.cvc	163	log plain
-rw-r--r--	constarr2.smt2	296	log plain
-rw-r--r--	incorrect1.smtv1.smt2	5447	log plain
-rw-r--r--	incorrect10.smtv1.smt2	20746	log plain
-rw-r--r--	incorrect11.smtv1.smt2	2464	log plain
-rw-r--r--	incorrect2.minimized.smtv1.smt2	354	log plain
-rw-r--r--	incorrect2.smtv1.smt2	10404	log plain
-rw-r--r--	incorrect3.smtv1.smt2	13832	log plain
-rw-r--r--	incorrect4.smtv1.smt2	4829	log plain
-rw-r--r--	incorrect5.smtv1.smt2	9991	log plain
-rw-r--r--	incorrect6.smtv1.smt2	43266	log plain
-rw-r--r--	incorrect7.smtv1.smt2	1917	log plain
-rw-r--r--	incorrect8.minimized.smtv1.smt2	453	log plain
-rw-r--r--	incorrect8.smtv1.smt2	33913	log plain
-rw-r--r--	incorrect9.smtv1.smt2	5140	log plain
-rw-r--r--	issue3813-massign-assert.smt2	205	log plain
-rw-r--r--	issue3814.smt2	296	log plain
-rw-r--r--	issue4927-unsat-cores.smt2	332	log plain
-rw-r--r--	swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2	1448	log plain
-rw-r--r--	x2.smtv1.smt2	342	log plain
-rw-r--r--	x3.smtv1.smt2	875	log plain