A theorem prover shootout, in the spirit of The Great Computer Language Shootout, for challenging verification problems that occur in practice.
The current focus is on real-world (not synthetic) mixed bitvector and arithmetic problems. We welcome pull requests of new problems, and solutions to existing problems in different solvers.
- Each problem is a toplevel directory, such as
P1/. - Each solution for a given theorem prover is a subfolder, such as
P1/lean.