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.