[SMTCOMP] The infinite-precision issue again

[Leonardo de Moura]

Hi Hyondeuk,


> I don't understand the difference between the original SMT  
> benchmarks and the
> new submitted benchmarks.

There is no difference between original and new benchmarks.
The benchmark selection algorithm does not distinguish between old  
(original) and
new 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.

Some of the new benchmarks are also from the real-world and some of  
them are
also hand-maded.


> I also believe
> that the current benchmark is somewhat biased; for example, most of  
> them are
> unsat problem.


I agree SMT-LIB has more unsat than sat benchmarks, but several new  
SAT instances
were included this year. Moreover, the benchmark selection algorithm  
tries to produce (when
possible) a balanced distribution of benchmarks: 25% easy-sat, 25%  
easy-unsat,
25% hard-sat, 25% hard-unsat.


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


We are using all submitted benchmarks. If some benchmarks are missing  
from
the revised library, then please tell us.

Leonardo