Different error report from first example

[tlringer]

Hello, I'm going through the tutorial and I just want to report any discrepancies I encounter. When I run the first example I get a different error report from the one described in the tutorial. Mine has the values:

y | -2147483647i32 x | -2147483648i32

instead. Does CN just give you any one example in an error report, rather than a specific one? Is there nondeterminism involved in what examples might be presented in the error report? If so, I think this should be clarified in the tutorial, otherwise it is easy to get lost already at this point.

[tlringer]

Oh, I see a small parenthetical about this in the tutorial. I missed it the first time. Can we make it more prominent, or move it earlier? Otherwise I see a mismatch and just assume something has already gone wrong.

[tlringer]

Specifically I would put that parenthetical at the top where it says "the report comprises two sections" because the second I see the mismatch, I am going to get confused.

[tlringer]

Also, my only constraints are:

repr<void*>(__builtin_ctzl)
repr<void*>(__builtin_ctzll)
repr<void*>(add)
aligned(&ARG0, 4u64)
aligned(&ARG1, 4u64)

Accordingly, I have no idea what this is referring to:

For instance, good<signed int>(x) says that the initial value of x is a “good” signed int value (i.e. in range). Here signed int is the same type as int, CN just makes the sign explicit. For integer types T, good<T> requires the value to be in range of type T; for pointer types T it also requires the pointer to be aligned. For structs and arrays this extends in the obvious way to struct members or array cells.

I assume the constraints can also vary depending on the version of Z3 installed? I would just put this all at the very top of the section and say the specific error report you see for the same function might vary depending on the version of Z3 installed.