Fixed an unsoundness where the condition of a while statement was not checked for arithmetic overflow.
Fixed an unsoundness where the condition of a while statement was not checked for arithmetic overflow.

willempx/verifast,willempx/verifast,willempx/verifast,willempx/verifast,willempx/verifast