Byte-extract operations on pointer arrays can produce incorrect constraints?

[smowton]

See comments on #188; opening this to track a different possible bug involving byte-extract operations and array constraints.

[smowton]

Further observations:

• If the latest program in Pointer_offset misuse in value_set_dereference.cpp? #188 is rewritten to use void** everywhere (so all array indexing uses void** and only elements are cast) it gives the incorrect solution { .x=0, .x=0 }
• If it is rewritten instead to use unsigned long* it gives the correct answer!

[kroening]

Please check whether 7d78d58 fixes this.

[smowton]

Seems fixed.