PV4 ⊧ SPASS-SATTproduces a satisfiability result for a formula

a complete solver for ground linear arithmetic

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

Format:

a subset of the SMT-LIB standard v2.6

Internals

Supported theories are QF_LRA (ground linear rational arithmetic), QF_LIA (ground linear integer arithmetic), and QF_LIRA (ground linear mixed arithmetic). The theory solver used by SPASS-SATT is called SPASS-IQ.