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

[Roberto Bruttomesso]

Hello,

the benchmarks have been fixed and are available from

http://smtcomp.sourceforge.net/2012/application.shtml

Please let me know if you encounter other issues

Regards,
Roberto

On Fri, Jun 1, 2012 at 9:43 AM, Roberto Bruttomesso
<roberto.bruttomesso at gmail.com> wrote:
> 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



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