[SMT-LIB] Version 2.0 of SMT-LIB is finally here!

[geoff@cs.miami.edu]

Hi Cesare, all,

> we are pleased to announce that, after a very long gestation, we are very close to finalizing Version 2.0 of the SMT-LIB standard. An almost final draft of the reference document is available at
> 
> http://www.smt-lib.org/papers/v2-ref-manual-draft.pdf
> 
> The document has been prepared with the input and feedback of three working groups, consisting of SMT researchers, developers and power users. 
> 
> We encourage interested people in this wider list to take a look at the document and give us their feedback **by the end of this month.**

I don't know if I mentioned this before, but I encourage you to consider 
using the SZS ontology for system result values ...
    http://www.tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology
... instead of the unsupported | success | error, timeout | memout | 
incomplete, and sat | unsat | unknown values currently listed. The ontology 
supports more fine grained reporting, and has a sound semantic basis. There 
is a paper about it at ...
    http://www.cs.miami.edu/~geoff/Papers/Conference/2008_Sut08_KEAPPA-38-49.pdf

Generally, it looks like SMT is ready to conquer the world!

Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------