[SMT-LIB] Version 2.0 of SMT-LIB released

[Cesare Tinelli]

Dear all,

we are happy to announce the first release of Version 2.0 of the SMT-LIB format.

The reference document is available in the documents section of the SMT-LIB website (http://www.smt-lib.org).

We will be working on migrating the whole library (theories, logics and benchmarks) to the new format next, for the next few weeks, to give SMT solver writers benchmarks to test their upgraded systems on. We'll keep you posted on our progress.


Thanks to your feedback, the final document improves on the latest draft in several ways. Unfortunately, it also removes a number of features and commands that we felt needed further discussion or greater consensus within the relevant working groups. Our intention is to introduce them, and possibly others, as soon as possible in Version 2.1. 

As with any major new version, the reference document can be still improved in a number of ways. We plan to do that in the next months, as time permits. In the meantime, additional feedback on it is always welcome.

This was truly a collective effort. We sincerely thank everybody who contributed their ideas, suggestions, comments and proof-reading. We think we have listed all significant contributors in the document's acknowledgments. If we have forgotten anybody please do let us know.


Aaron, Clark and Cesare