<div dir="ltr">Is it reasonable to assume in the analyzer that a symbol representing the extent<br>of an analyzed memory region can not be greater then size_t_max/2?<br><br>If so, why does the constraint manager not know about this fact?<br>If not, why does the `ProgramState::assumeInBound` still heavily exploit this<br>fact in its implementation?<br><br>Without deciding this Z3 refutation will not be able to filter as many false<br>positives as it potentially could.<br><br>Regards,<br>Balazs</div>