[SMT-COMP] QF_BV: Division by zero

[Clark Barrett]

Robert,

I apologize for not responding to this sooner.  We do have a plan for dealing
with this issue.

CVC3 has the capability to generate a Type Correctness Condition (TCC) for
these benchmarks.  The TCC is a formula which, if valid, indicates that the
validity of the benchmark cannot depend on how division by zero is defined.  If
invalid, it means that the definition of division by zero could affect the
validity of the benchmark.  The algorithm for generating TCC's is described in
an old PDPAR paper:

Berezin et al., A Practical Approach to Partial Functions in CVC Lite.
http://www.cs.nyu.edu/~barrett/pubs/BBS+05.ps

Our plan is to generate TCC's for all benchmarks containing division
operators.  We will then use multiple tools to check the validity of the TCCs.
All benchmarks whose TCCs are valid will be included in the competition.  The
others will be rejected.

Questions and feedback on this plan are welcome.

-Clark


> 
> 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
> 
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>