title: "Taking on a Challenge in SPARK Ada" - Sum ghost function in post-condition having unintended behavior
body: <p>I am writing a piece of software in SPARK Ada which requires the post-condition to verify that the function return value is equal to the summed values of an array. Upon proving the file where the function resides, I keep getting an error which doesn't quite add up, no pun intended (I will post screenshots of the code so as to allow a better look). The only acceptable values allowed in the array of size 10 are 0s or 1s.</p>
  <p><a href="https://i.stack.imgur.com/SFD4o.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/SFD4o.png" alt="enter image description here" /></a></p>
  <p><a href="https://i.stack.imgur.com/FOIhR.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/FOIhR.png" alt="enter image description here" /></a></p>
  <p><a href="https://i.stack.imgur.com/qHZyw.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/qHZyw.png" alt="enter image description here" /></a></p>