Initial document on SMT-LIB 3.0

[Cesare Tinelli]

Hi everybody,

As many of you know, we, the SMT-LIB coordinators, have been working for a while on Version 3 of the SMT-LIB standard.

The main feature of the new version is the move to simply-typed higher-order logic as the underlying logic of SMT-LIB. This is achieved as a largely backward-compatible extension of Version 2.6.

We have made substantial progress towards defining our proposal for Version 3, based on feedback we already gathered from direct interactions with members of the community. We are working on a reference document that will describe it at the same level of detail as the reference document for Version 2.6.

In the meantime, we have prepared a web page with highlights on the new version, with the hope of gathering additional feedback from you. The page is work in progress and will be expanded and updated over time. However, your feedback, on this list or by other means, is already welcome.

Thanks,

Cesare, Clark & Pascal