Fatal Error: BVConstEvaluator:division by zero error

[Jonas Wagner]

Hi,

running the attached query using the latest version (revision 1668) of STP yields to the following error message:

Fatal Error: BVConstEvaluator:division by zero error

Any ideas where this might come from?

Best,

Jonas

[Vijay Ganesh]

Hi Jonas,

A quick look at your constraint shows that it is possible for the
denominator of BVMOD (modulo operation) to take the value zero.

-Vijay.

> --
>
>
>



--
Vijay Ganesh.
http://ece.uwaterloo.ca/~vganesh

[Jonas Wagner]

Hello,

thanks Vijay for your answer, and sorry for the late reply.

A quick look at your constraint shows that it is possible for the
denominator of BVMOD (modulo operation) to take the value zero.

Do you mean the b_1 value? This shouldn't be possible. Let me explain.

The query comes from verifying a program that computes the GCD of two numbers. It goes as follows:

unsigned int gcd(unsigned int a, unsigned int b) {

    assume(a > 0 & a < 20 & b > 0 & b < a);

    int old_a = a, old_b = b;

    while (b != 0) {

        int r = a % b;

        a = b;

        b = r;

    }

    // Check that a is indeed a divisor

    assert((old_a % a == 0) & (old_b % a == 0));

    // Check that no other divisor is larger

    int other = NONDET_INT();

    assume(other > 0);

    // FIXME: STP crashes on this

    assert((other <= a) | (old_a % other != 0) | (old_b % other != 0));

    return a;

}

If I'm not mistaken, this precludes any possibility of a divisor being zero. Also, I believe that the constraint is reflected faithfully in the query:

- The first ASSERT in the query corresponds to the first assume statement in the program

- The second ASSERT seems to be the condition for exiting the loop

- The fourth ASSERT corresponds to assume(other > 0)

- The final ASSERT corresponds to the last assert statement

I've simplified the query a bit by reducing the number of loop iterations; it's attached again.

Also, note that this program is verified if we use boolector or Z3, it only fails when using STP (but let's add that STP is much faster than the others ;-))

Cheers,

Jonas

[Vijay Ganesh]

Hi Jonas,

Okay, I will have to get back to you on this. I am currently traveling
till Nov 12th. I will look into this when I get back.

-Vijay.