nl « 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--	all-logic.smt2	105	log plain
-rw-r--r--	coeff-sat.smt2	211	log plain
-rw-r--r--	iand-no-init.smt2	106	log plain
-rw-r--r--	issue3003.smt2	598	log plain
-rw-r--r--	issue3407.smt2	152	log plain
-rw-r--r--	issue3411.smt2	184	log plain
-rw-r--r--	issue3475.smt2	168	log plain
-rw-r--r--	issue3652.smt2	195	log plain
-rw-r--r--	issue3718.smt2	117	log plain
-rw-r--r--	issue3719.smt2	103	log plain
-rw-r--r--	issue3729-cm-solved-tf.smt2	160	log plain
-rw-r--r--	issue3959.smt2	275	log plain
-rw-r--r--	issue3971.smt2	12766	log plain
-rw-r--r--	issue3991.smt2	290	log plain
-rw-r--r--	issue4007-rint-uf.smt2	179	log plain
-rw-r--r--	issue5534-no-assertions.smt2	234	log plain
-rw-r--r--	issue5726-downpolys.smt2	238	log plain
-rw-r--r--	issue5726-sqfactor.smt2	239	log plain
-rw-r--r--	issue5737-div00.smt2	124	log plain
-rw-r--r--	issue5740-2-mod00.smt2	325	log plain
-rw-r--r--	issue5740-mod00.smt2	216	log plain
-rw-r--r--	magnitude-wrong-1020-m.smt2	2585	log plain
-rw-r--r--	mult-po.smt2	335	log plain
-rw-r--r--	nia-wrong-tl.smt2	1229	log plain
-rw-r--r--	nlExtPurify-test.smt2	843	log plain
d---------	nta	397	log plain
-rw-r--r--	real-as-int.smt2	234	log plain
-rw-r--r--	real-div-ufnra.smt2	280	log plain
-rw-r--r--	sin-cos-346-b-chunk-0169.smt2	666	log plain
-rw-r--r--	sqrt.smt2	595	log plain
-rw-r--r--	sqrt2-value.smt2	238	log plain
-rw-r--r--	subs0-unsat-confirm.smt2	383	log plain
-rw-r--r--	tpp-fail-pf-012921.smt2	132	log plain
-rw-r--r--	very-easy-sat.smt2	1041	log plain
-rw-r--r--	very-simple-unsat.smt2	293	log plain