uflra « 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--	bug293.cvc	131	log plain
-rw-r--r--	bug449.smtv1.smt2	203	log plain
-rw-r--r--	constants0.smtv1.smt2	468	log plain
-rw-r--r--	fuzz01.smtv1.smt2	8313	log plain
-rw-r--r--	incorrect1.delta01.smtv1.smt2	459	log plain
-rw-r--r--	incorrect1.delta02.smtv1.smt2	179	log plain
-rw-r--r--	neq-deltacomp.smtv1.smt2	210	log plain
-rw-r--r--	pb_real_10_0100_10_10.smtv1.smt2	9176	log plain
-rw-r--r--	pb_real_10_0100_10_11.smtv1.smt2	9545	log plain
-rw-r--r--	pb_real_10_0100_10_15.smtv1.smt2	9668	log plain
-rw-r--r--	pb_real_10_0100_10_16.smtv1.smt2	9195	log plain
-rw-r--r--	pb_real_10_0100_10_19.smtv1.smt2	8866	log plain
-rw-r--r--	pb_real_10_0200_10_22.smtv1.smt2	14349	log plain
-rw-r--r--	pb_real_10_0200_10_25.smtv1.smt2	13785	log plain
-rw-r--r--	pb_real_10_0200_10_26.smtv1.smt2	13782	log plain
-rw-r--r--	pb_real_10_0200_10_27.smtv1.smt2	13615	log plain
-rw-r--r--	pb_real_10_0200_10_29.smtv1.smt2	14025	log plain
-rw-r--r--	simple.01.cvc	71	log plain
-rw-r--r--	simple.02.cvc	116	log plain
-rw-r--r--	simple.03.cvc	181	log plain
-rw-r--r--	simple.04.cvc	249	log plain