[SMT-LIB] Final Benchmarks

[Domagoj Babic]

Hi Clark,

There seems to be a bug in some of the Calysto benchmarks:

For instance, bin_eventlogadm_vc331085.smt:1694 AND operator
has only one operand.

I'm pretty sure that my sf2smt tool doesn't generate such instances,
because I would have gotten the same failure on those instances before...
My guess is that it's your post-processing script.

It could be a bug in sf2smt, but I doubt it..

Regards,

-- 
        Domagoj Babic

        http://www.domagoj.info/



On 6/12/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> Greetings to the SMT-COMP and SMT-LIB communities.  As you know, we have been
> working on finalizing the new bitvector theories for a while.  I am happy to
> report that the new theories and logics have now been posted on the smtlib web
> site.  They are very similar to the last draft I circulated on these lists, the
> only changes being a correction to the definition of bvashr and removal of a
> copule of the more obscure operators.
>
> I am also happy to report on the successful translation of over 8000 benchmarks
> into the new QF_BV and QF_AUFBV logic formats.  I was hoping to get these done
> sooner, but as you can imagine, getting that many benchmarks translated is
> quite challenging (there are always unexpected problems).
>
> Curiously, we actually have no benchmarks in the QF_UFBV category.  The
> benchmarks from last year have been retranslated and they all landed either in
> QF_BV or QF_AUFBV.
>
> Currently the plan for the competition is to have two bitvector divisions
> (QF_BV and QF_AUFBV) and to use all the benchmarks in QF_BV and QF_AUFBV.
> Since this will require changes to parsers and algorithms, let me know now if
> anyone has a big problem with this.  The format has been available for some
> time, so hopefully you've already started making the necessary modifications.
>
> This also represents the last changes to the benchmarks before the competition
> (modulo any errors that are found).
>
> Happy benchmarking!
>
> -Clark
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>