Implicitly constrain symbolic pointers to region 0 when adding offset constraints

[danmatichuk]

The set of identifiers sent to the front end contains separate identifiers for the offset and region for any symbolic pointer. If the user provides a constraint for a pointer offset, they almost certainly intend for that value to be either interpreted as a raw bitvector or an absolute pointer. In both of these cases, the region for that pointer should be constrained to 0, to avoid creating unexpected models where the pointer is concretized to an offset in a dynamic allocation.

Currently we always try to generate a model which assumes a collection of pointer correctness axioms (e.g. comparing two pointers implies they must have the same region), and so in many cases we should end up with reasonable models even without this explicit constraint, but this will ensure it gets added even when those axioms can't be inferred.