[SMTCOMP] The infinite-precision issue again

[Hyondeuk.Kim@colorado.edu]

Hello Albert and Leonardo,

I don't understand the difference between the original SMT benchmarks and the
new submitted benchmarks. As Albert mentioned in his paper, the orignal
benchmarks are from the real world and some of them are hand-maded. I believe
that the new submitted benchmarks are also from the real world. I also believe
that the current benchmark is somewhat biased; for example, most of them are
unsat problem. SMT-LIB encourage people to submit new benchmarks. If the new
set of benchmarks are not used in SMT COMP, this does not meet the objective
of SMT LIB.

I would like to hear your opinion about this.

Thank you.

Hyondeuk


Quoting Leonardo de Moura <demoura at csl.sri.com>:

> Hi Albert,
>
>
> > I followed with interest the discussion about the infinite-
> > precision issue and was satisfied with the conclusions obtained.
> > However, I am a little bit surprised after the final set of
> > benchmarks has been published.
>
> On June 10, I posted an email describing Aaron's, Clark's, and my
> position about this issue.
> In the end of the email, we said:
>
>
> >> That said, we will enforce that (where applicable) each division
> >> contains
> >> at least one benchmark that requires bignums, kind of like we did
> >> with
> >> integers last year.  That way, people have some incentive to move to
> >> multi-precision arithmetic.
>
>
> Since nobody complained, we assumed everybody was happy with this
> decision.
>
>
> > For all these reaons, I would suggest to remove the artificially
> > added benchmarks from those divisions. However, of course, I am
> > **very** interested in knowing what other people think about this
> > issue.
>
> I understand your reasons, and I am also interested in knowing what
> others think about this
> issue.
>
> Cheers,
> Leonardo
>
>
>
>
>
>
>