division by zero false-report

[necto]

This may be a duplicate of #206 . In fact the query under consideration is the Klee query, simplified for readability and fed to STP CLI. To this query:

x  : ARRAY BITVECTOR(4) OF BITVECTOR(4);
%----------------------------------------------------
ASSERT( NOT(0x0 = SBVREM(4, x[0x0], 0x2)) );
ASSERT( NOT(0x0 = SBVREM(4, 0x1, x[0x0])) );
%----------------------------------------------------
QUERY( NOT(0x0 = x[0x0]) );

STP responds with:

WARNING
Fatal Error: division by zero error
stp: Error: division by zero error

Why is it the case? As I understand the first ASSERT ensures that x[0x0] is never even, so it is definitely not 0.

[necto]

The query can be simplified further:

x  : BITVECTOR(4);
%----------------------------------------------------
ASSERT( NOT(0x0 = x) );
ASSERT( NOT(0x0 = SBVREM(4, 0x1, x)) );
%----------------------------------------------------
QUERY( NOT(0x0 = x) );

[msoos]

First of all, thanks for the bugreport! What's even more interesting:

x  : BITVECTOR(4);
ASSERT( NOT(0x0 = SBVREM(4, 0x1, x)) );
QUERY( NOT (0x0 = x) );

then:

$ ./stp -p tmp.cvc 
WARNING
Fatal Error: division by zero error
stp: Error: division by zero error

which probably makes this much more understandable. What is happening is that the x is the divisor, so if it's 0, STP goes upside down. The issue is that by having the query "NOT(0x0x = x)" STP tries to prove that this query is false by setting x to 0 and trying to find a solution. So it sets x to 0 and propagates this fact. It then hits the wall.

Yes, this is an issue and wrong behaviour. And it is exactly the same issue as before with division by zero :( We are thinking about how to resolve this. It's non-trivial, actually.

[TrevorHansen]

As per #223 , this no longer crashes, but dividing by zero might not behave like you expect.