Reach verifier not working correctly

[hckoseoglu]

Even though I ensure some conditions with checks which I will describe further, reach verifier gives errors using examples that are not complying to the check constraints

I have attached the code and the error message is below.
Even though it makes sure that each share should be less than 10.000 with the following code:

require(royaltyArr.all(x => x.share <= TOTAL_SHARE));

where total share is equal to 10.000

verifier gives the following as an example:

// ^ could = array(Object({"claimable": UInt, "share": UInt, "stakeholder": Address}), [{claimable: 115792089237316195423570985008687907853269984665640564039457584007913129629935, share: 10002,

which is impossible.

The code is attached below.
auto-claim.txt

[jeapostrophe]

The only thing that is known inside of while loops (like parallelReduce) about loop variables (like royalties) is what is in the invariant. You should put the claim about their total share in the invariant.