SMT-Solving Induction Proofs of Inequalities Benchmarking Repository

This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper: A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices. The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time.Part of this repository was submitted to the 2022 SMT-LIB benchmarks: https://github.com/SMT-LIB/benchmark-submission-2022/tree/master/non-incremental/QF_NRA/20220314-Unc