This repository contains benchmarks and challenge problems for inductive theorem provers. The benchmarks are written in a superset of SMTLIB under the benchmarks/ directory and its subdirectories. Each file contains exactly one problem.

The benchmarks under the false/ subdirectory are false properties, meant as benchmarks for counterexample-finding tools.

The original directory contains the original Haskell source files for many of the problems.

The benchmarks are also available to download in Why3 format, and a CVC4-compatible version of SMTLIB:

• Why3: http://tip-org.github.io/tip-benchmarks-0.2-why3.tar.gz
• CVC4: http://tip-org.github.io/tip-benchmarks-0.2-cvc4.tar.gz
• TIP format: http://tip-org.github.io/tip-benchmarks-0.2.tar.gz

After installing the TIP tools you can generate the whole problem set in TIP, Why3 and CVC4 format yourself from the Haskell sources. To do this run omake. This may be useful if you want to add your own problems, but it is not a requirement that they come from a Haskell source file.

Contributions are most encouraged! Any inductive problem, big or small, simple or difficult is welcome.

The simplest method to add new benchmarks is via a github pull request to this git repo, adding the problems to the originals/ directory in either Haskell or TIP format. We can take care of updating the build scripts to include your new problems.

We're also looking for non-theorem benchmarks to evaluate tools that find counterexamples to false properties.

You are also free to email the maintainers with new problems (or questions):

• Nick Smallbone [email protected]
• Moa Johansson [email protected]