nta « 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--	NAVIGATION2.smt2	680	log plain
-rw-r--r--	arrowsmith-050317.smt2	14137	log plain
-rw-r--r--	bad-050217.smt2	2854	log plain
-rw-r--r--	cos-bound.smt2	123	log plain
-rw-r--r--	cos-sig-value.smt2	156	log plain
-rw-r--r--	cos1-tc.smt2	132	log plain
-rw-r--r--	dumortier-050317.smt2	11594	log plain
-rw-r--r--	dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2	4990	log plain
-rw-r--r--	exp-4.5-lt.smt2	156	log plain
-rw-r--r--	exp-n0.5-lb.smt2	179	log plain
-rw-r--r--	exp-n0.5-ub.smt2	178	log plain
-rw-r--r--	exp1-lb.smt2	184	log plain
-rw-r--r--	exp1-ub.smt2	185	log plain
-rw-r--r--	exp_monotone.smt2	303	log plain
-rw-r--r--	shifting.smt2	334	log plain
-rw-r--r--	shifting2.smt2	368	log plain
-rw-r--r--	sin-compare-across-phase.smt2	173	log plain
-rw-r--r--	sin-compare.smt2	203	log plain
-rw-r--r--	sin-init-tangents.smt2	174	log plain
-rw-r--r--	sin-sign.smt2	201	log plain
-rw-r--r--	sin-sym.smt2	191	log plain
-rw-r--r--	sin-sym2.smt2	287	log plain
-rw-r--r--	sin1-lb.smt2	184	log plain
-rw-r--r--	sin1-ub.smt2	185	log plain
-rw-r--r--	sin2-lb.smt2	183	log plain
-rw-r--r--	sin2-ub.smt2	184	log plain
-rw-r--r--	tan-rewrite.smt2	201	log plain
-rw-r--r--	tan-rewrite2.smt2	236	log plain