Tree Interpolation in Vampire

Vampire now supports the computation of tree and sequence interpolants.

Input files

Vampire reads tree interpolation problems compatible with the SMT-LIB 1.2 format, using the input standards introduced in iZ3.

Tool usage

For computing tree interpolants in Vampire, one should simply invoke Vampire on the command line as follows:


You can download the x86 Linux version of Vampire (version 1.8) here. Store all files of the archive in the same directory.

To get the most recent updates of Vampire, visit the Vampire page!


We evaluated tree interpolation in Vampire using two benchmark suites: