[SMTCOMP] IMPORTANT: the infinite-precision issue

[Roberto Sebastiani]

Dear colleagues,

there is an important question about SMT-COMP which apparently 
nobody asked so far: do we explicitly require infinite precision 
from SMT solvers on arithmetic-related theories? 
(I.e., RDL/IDL/LAR/LAI and combinations.)

On the one hand, infinite precision prevents an SMT tool from
giving wrong answers on some problems. On the other hand, using 
infinite precision significantly slows down the performances 
(around a 3 factor in our experience).

Thus, we believe that, in order to guarantee a fair comparison,
this issue should be decided a priori and clearly stated in the 
competition rules. In particular:

1 if we require infinite precision, then the benchmarks of all categories
   should contain  a significant amount of problems (even very easy ones)
   which cause wrong answers if dealt with non-infinite arithmetic;

2 if we do not require infinite precision, then this must be decided a
   priori and clearly stated in the rules, so that tools using infinite
   precision can decide with a reasonable advance to use standard
   arithmetic instead.


Roberto





-- 
------------------------------------------------------------------
Prof. ROBERTO SEBASTIANI
Dip. Informatica e Telecomunicazioni
Fac. Scienze M.F.N., Universita` di Trento    Tel: +39 0461 881514
Via Sommarive 14, I-38050, Trento, Italy      Fax: +39 0461 882093
roberto.sebastiani at dit.unitn.it     http://www.dit.unitn.it/~rseba
------------------------------------------------------------------