Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

SMT-LIB format

The SMT-LIB input format is described on the SMT-LIB web site: SMT-LIB input format.

The Native Z3 format re-uses the function names used in SMT-LIB. A table of the relevant function names is summarized in the documentation for Z3 theories.