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

Format:

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

Expected output

sat, unsat or unknown

Internals

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.
SMT

Links

Last commit date

22 September 2021

Related papers

Last publication date

12 January 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.