[SMT-LIB] Final Benchmarks

[Clark Barrett]

Good catch.  It's my fault: I had to run your benchmarks through my translator
to clean up a few small consistency issues.  However, at the same time, it
seems to have replaced references to "distinct" with conjunctions of
disequalities.  This was unintentional.  I'll post a correction soon.

-Clark

> 
> 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
> >
>