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

[Juergen Christ]

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.

Regards,

Juergen