Slight refinement: don't havoc variables that are not changed.
Some prep work for adding size information to the constraint.
Add size bound constraints.