maxandsum.adb:11:10: info: loop invariant initialization proved[#13]
maxandsum.adb:11:10: info: loop invariant preservation proved[#14]
maxandsum.adb:11:33: info: initialization of "Sum" proved[#4]
maxandsum.adb:11:50: info: initialization of "Max" proved[#5]
maxandsum.adb:12:17: info: initialization of "Sum" proved[#6]
maxandsum.adb:12:21: info: overflow check proved[#12]
maxandsum.adb:13:13: info: initialization of "Max" proved[#7]
maxandsum.adb:16:25: info: initialization of "Sum" proved[#8]
maxandsum.adb:16:25: medium: assertion might fail, requires Sum <= I * Max[#11]
maxandsum.adb:16:36: info: initialization of "Max" proved[#9]
maxandsum.ads:11:43: info: initialization of "Sum" proved[#0]
maxandsum.ads:11:62: info: initialization of "Max" proved[#1]
maxandsum.ads:12:19: info: initialization of "Sum" proved[#2]
maxandsum.ads:12:19: info: postcondition proved[#10]
maxandsum.ads:12:30: info: initialization of "Max" proved[#3]
