Division by zero error

[Edward Schwartz]

The attached stp formula produces the following error:

Fatal Error: BVConstEvaluator:division by zero error

There is division in the formula, but the divisor is symbolic, and
does not have to be zero. I think it is a bug.

Thanks,

Ed

[Trevor Hansen]

Hi Edward,

> The attached stp formula produces the following error:

>    Fatal Error: BVConstEvaluator:division by zero error

Thanks for the bug report.

STP's implementation of division in the CVC language is to not allow division by zero. That is, STP produces an error if a division by zero occurs in the counter-example.  I don't know what the semantics should be for the language. In the CVC3 user guide  ( http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html ), when x is a real,  they evaluate x/0 to zero. So maybe we should do the same for bit-vectors, I've not changed the semantics for division by zero because I don't know if anyone relies on the current semantics.

For input in the SMT-LIB1 and SMT-LIB2 languages, STP breaks with the official semantics and defines x/0 as 1, and x%0 as x.

If these semantics don't seem right to you, let me know what you think they should be,

Best,

Trevor.

[Ed Schwartz]

On Sun, Mar 25, 2012 at 8:45 PM, Trevor Hansen
<tha...@csse.unimelb.edu.au> wrote:
> Hi Edward,
>
>> The attached stp formula produces the following error:
>
>>    Fatal Error: BVConstEvaluator:division by zero error
>
> Thanks for the bug report.
>
> STP's implementation of division in the CVC language is to not allow
> division by zero. That is, STP produces an error if a division by zero
> occurs in the counter-example.  I don't know what the semantics should be
> for the language. In the CVC3 user guide  (
> http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html ), when x is a real,
> they evaluate x/0 to zero. So maybe we should do the same for bit-vectors,
> I've not changed the semantics for division by zero because I don't know if
> anyone relies on the current semantics.
>
> For input in the SMT-LIB1 and SMT-LIB2 languages, STP breaks with the
> official semantics and defines x/0 as 1, and x%0 as x.
>
> If these semantics don't seem right to you, let me know what you think they
> should be,

Hi Trevor,

I think these semantics are okay; there does not seem to be a "right"
semantics for this. However, maybe the error message should specify
that division by zero is an error in the semantics. I was expecting
smtlib/cvc3 semantics for division, so when I saw the BVConstEvaluator
message, I thought it was a bug, rather than a semantics decision.

Thanks,
Edward