Do not produce impossible models for symbolic strtol
Do not produce impossible models for symbolic strtol

Previously, if the strtol conversion reached the limit for number of
bytes, it would not add a constraint on the terminating byte. This
resulted in models which did not process the same in a real strtol if
the next byte happened to be satisfied by a digit. Notably this was
observed with z3 4.8.0 running test_strtol.

Also clarifies comments. I don't know what we did to deserve the hellish
fury of symbolic string conversions.

angr/angr,angr/angr,iamahuman/angr,schieb/angr,iamahuman/angr,schieb/angr,schieb/angr,iamahuman/angr,angr/angr