[SMT-COMP] QF_BV: Division by zero

[Robert Wille]

Dear all,

 

we have a question regarding the benchmarks of the QF_BV division. Last year
there was a discussion about how to handle the division operator (in
particular, how to handle division by zero). Since this issue couldn't be
completely clarified, all benchmarks including divisions have been removed
from the QF_BV-set for the competition. Now, the new benchmark set for
SMTCOMP'09 again include benchmarks with division operations. Thus, it would
be interesting if there is a new status of the discussion? If yes, could
someone please link us to the respective thread/post, where this is
described?

 

Many thanks in advance,

Robert Wille