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


a subset of the SMT-LIB standard v2.6


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.


Project page: https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/spass-satt

ProVerB specific

Markdown description: view/edit

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