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

[Roberto Bruttomesso]

Hi,

thanks for spotting this. We will shortly regenerate the benchmarks.

Regards,
Roberto

On Thu, May 31, 2012 at 6:54 PM, Juergen Christ
<christj at informatik.uni-freiburg.de> wrote:
> 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
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp



-- 
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70