[SMT-LIB] Quoting fixes in SMT-LIB

[Morgan Deters]

Hi SMT-LIB and SMT-COMP communities,

We have become aware of some additional problems with the SMT-LIB
benchmarks having to do with improper (missing) quoting in symbols
containing tick characters (').

For example, the following was observed in many benchmarks:

  (declare-fun status' () Int)

where to be spec-conformant, the symbol must be quoted with |:

  (declare-fun |status'| () Int)

There were roughly 1800 benchmarks with this problem; they have been
fixed in the benchmark library, and the new benchmark revision will be
available on SMT-Exec soon as "20100619-smtlib2".

As usual, the benchmarks are available from

   http://www.smtlib.org/

All changes to the library can be seen (and just these changes
downloaded) by using the SMT-LIB benchmark search interface and
searching for:

   modified >= 2010-06-19

These benchmarks will also be available on SMT-Exec shortly (within an
hour or so) as benchmark revision '20090618-smtlib2'.

The changes affect the following benchmark families:

  AUFLIA/boogie
  AUFLIA/sexpr
  AUFLIA/simplify2
  AUFLIA/tokeneer
  QF_IDL/sep
  UFNIA/spec_sharp

Regards,
Morgan (also for Albert, Clark, Aaron, and Cesare)