PV4 SMTInterpolproduces a satisfiability result for a formula

SMT solver that can compute Craig interpolants for various theories

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula


SMT-LIB v2.6 It supports Craig interpolation via an extension of the SMT-LIB format.

Expected output

sat, unsat or unknown


It supports the combination of the theories of uninterpreted functions, linear real arithmetic, linear integer arithmetic, arrays including constant arrays, and datatypes. It supports quantifiers for all supported theories except for datatypes. It supports interpolation for the quantifier-free fragments of all supported theories except datatypes.


Related papers

Last publication date

12 January 2021

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.