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
