[SMTCOMP] The infinite-precision issue again

[Albert Oliveras Llunell]

Dear colleagues,

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.

My surprise concerns all divisions related with difference logic 
(QF_RDL, QF_IDL and QF_UFIDL). To the best of my knowledge most solvers 
for DL are based on negative-cycle detection or shortest-path 
computation. With all these algorithms, and unlike with Simplex-like 
methods, infinite precision is not an issue: if one adds all the 
integers appearing in the input formula and an overflow is not produced, 
then one can be sure that infinite-precision is not needed. And this is 
what happens in all benchmarks (correct me if I am wrong) in those 
divisions except for the artificially introduced benchmarks.

As far as I know, the DL division was created because it had been widely
proved that DL was powerful enough to express interesting problems but 
it was much more efficient than full linear arithmetic. Now, forcing 
infinite-precision in DL seems like incentivating people to develop less 
efficient solvers for a set of benchmarks (DL where infinite precision 
is needed) which, after two years of collecting benchmarks, is still 
empty. I was assuming when the final decision was made that this year
there would be new real benchmarks with the infinite-precision 
requirement, but this does not seem to be the case.

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.

Best wishes,
Albert