[SMTCOMP] The infinite-precision issue again

[Leonardo de Moura]

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