Re: [Smtcomp-discussion] benchmarks involving divide by zero

[Mate S. <soo...@gm...>]

Dear All,

On 06/12/2014 01:36 PM, Alberto Griggio wrote:
>> After changing the satisfiability numerous solvers return wrong verdicts.
>> Take for QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2:
>> Wrong are:
>> * MathSAT5 5.2.12
>> * Boolector 1.6.0
>> * SONOLAR
>> * STP (master branch)
>> * Z3 (master branch)
>> Correct are:
>> * CVC4 1.3
>>
>> Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0
>> 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior.
> 
> MathSAT too, FWIW.
> 
>> I do not understand why this behavior should not be compliant. The logic
>> description of QF_BV merely states that bvudiv is "undefined if divisor
>> is 0".

STP can even crash on this: https://github.com/stp/stp/issues/106  due
to the undefinedness. The issue can be easily fixed, but as the
discussion there shows, nobody really knows what to do. Would be nice to
know what is the 'correct' behaviour where the SMT community defines
what is correct.

Cheers,

Mate