Hi Stefan,
The invariant you mention should indeed hold. I've never seen a
violation on a 32-bit machine. But I encountered a similar issue on
64-bit, where I think the next address should have been none. I don't
have time to debug this any further, but let me know if you do.
Best,
Hi,
I've just run into a Klee out of bound pointer error which I believe
it is actually not a bug in the program I'm testing, but some error in
Klee.
I tried to analyze the associated test.ptr.err file generated, but I
don't quite understand the meaning of next and prev addresses in
the
