This is very similar to the version that competed in CASC-30.

Pre-built Binaries

We offer pre-built binaries (including Z3) for common platforms below. These are new this release, so please tell us if they don't work for you. A source build is of course still possible - please use the provided tarballs rather than the GitHub sources. The pre-built binaries:

• are static for Linux systems
• dynamically link to the C++ runtime on Mac
• dynamically link to the C++ runtime and to Cygwin on Windows - we provide the Cygwin DLL we linked against, but others may work

Semantic Versioning

This is a major release mostly to coincide with The Vampire Diary (CAV 2025), but we intend to stick to semantic versioning in a very restricted sense from now on:

• The only supported interface is the default mode and the portfolio mode, --mode portfolio.
• Supported portfolio schedules are casc and casc_sat, e.g. --schedule casc: this list might be extended to other schedules in the future.
• The TPTP and SMT-LIB input formats are supported via --input_syntax tptp and --input_syntax smtlib2.
• The default output and the output flags -p tptp or -om smtcomp or -om ucore are supported.
• Runtime can be limited (with some margin of error) using -t <seconds>, where <seconds> is a positive integer.
• Vampire uses one CPU core in its default mode.
• All other options may break without warning.
• We do not guarantee solving any particular problem or returning any particular output, only that the above-enumerated ways of calling Vampire remain valid.

Most of our releases will be minor releases because we do not break the above, but may change, add or remove other functionality. Occasional point releases may occur in the event of disaster.