[SMT-COMP] Problem with the benchmarks for the unsat core track

[Alberto Griggio]

Hello Juergen (and others),

> Hi,
> 
> I just encountered a problem with the benchmarks for the unsat core 
track.
> Our solver refuses to accept the formulas since the formulas inside of 
the
> 
> :named annotation is not closed as required by the standard (page 25).  
The
> 
> benchmark smtlib/QF_LRA/check/bignum_lra2.smt2.uc.smt2 contains
> 
> (assert
> (let ((?def0 x6 ))
> (let ((?def1 (<= ?def0 0) ))
> (! ?def1 :named a__uc__1)
> ))
> )
> 
> One easy way to fix this is to lift the annotation:
> 
> (assert (!
> (let ((?def0 x6 ))
> (let ((?def1 (<= ?def0 0) ))
> ?def1)
> ) :named a__uc__1)
> )
> 
> I guess this problem occurs in all benchmarks.

Thanks for reporting! I have updated the benchmark scrambler so that it
is now possible to use it to fix the problem. The new scrambler is
available at:
  https://es.fbk.eu/people/griggio/smtcomp/smtcomp2012_scrambler.tar.gz 
(linked from http://smtcomp.sourceforge.net/2012/tools.shtml)

To fix the above issue, you can run the scrambler with the
"-lift_named_annot true" option, and with "-seed 0" to avoid scrambling.
Example:

  ./scrambler -seed 0 -lift_named_annot true < 
smtlib/QF_LRA/check/bignum_lra2.smt2.uc.smt2

We will fix the problem in the unsat core benchmarks as soon as
possible, but in the meantime you can do it on your local copy using the
scrambler. If you notice any other strange thing, please let us know.

Best,

Alberto