[SMT-LIB] Updates on SMT-LIB

[Tinelli, Cesare]

Hi all,

There has been a lot of work on the SMT-LIB initiative recently, at various levels. We will be sending several updates to this list in the next few weeks. The first are the following.

1) 
The SMT-LIB website has been completely revamped. Comments, corrections and suggestions are welcome.

2) 
We are in the process of moving the benchmark repository to the StarExec service and adding thousands of new benchmarks (a selection of which will be used for SMT-COMP'14). We will announce the new repository soon. In the meantime, we have disabled access to the old benchmark repository, which was hosted on the smtexec.org server. The old repository is however available on StarExec. See http://www.smt-lib.org/benchmarks.shtml for details.


3)
We have completed the definition of the syntax and semantics of an SMT-LIB theory of floating point numbers. The theory is available at http://www.smt-lib.org/theories.shtml
A number logics based on this theory will be added in the next few days.

We thank Martin Brain, Philipp Ruemmer and Thomas Wahl who played a major role in the definition of the theory. We also thank the following people who provided substantial feedback and directions: François Bobot, David Cok, Alberto Griggio, Florian Lapschies, Leonardo de Moura, Gabriele Paganelli, Cody Roux, and Christoph Wintersteiger.


Best,


Cesare, Clark and Pascal
The SMT-LIB coordinators