SPASS-SATT: A Ground Linear Arithmetic Solver

SPASS-SATT is a complete solver for ground linear arithmetic. The input language of SPASS-SATT is a subset of the SMT-LIB standard v2.6 that supports only the commands (set-logic L), (set-info A), (declare-const X T), (declare-fun X () T), (define-fun X () T F), (assert F), (check-sat), and (exit). 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.

Most recent version:
SPASS-SATT v 1.1   (Linux 64 bits AMD/Intel)

Older versions:
SPASS-SATT v 1.0   (Linux 64 bits AMD/Intel)

Please contact us for help, general questions, bug reports, etc.