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-SMT v 1.0 (Linux 64 bits AMD/Intel)
Please contact us for help, general questions, bug reports, etc.