Bug Coverage

[1nc0gn170]

Overview:

Set winner and Pause voting.

PR : https://github.com/Certora/tutorials-code/pull/6
BordaMissingRule.spec

A run of the new BordaMissingRule.spec on the original Borda.sol ->> https://prover.certora.com/output/547/9c7f0d95bde54d29b8d69e0ec27cfc51?anonymousKey=32f03dcc32835daf5c901e9306805db81ed9903c

A run of the new BordaMissingRule.spec on the BordaNewBug.sol ->> https://prover.certora.com/output/547/2160830e2fd74ebc8d40a8e3659aac42?anonymousKey=46ff60261303d503578de0fa3964c3eeafa9c512

A run of the new Borda.spec on the BordaNewBug.sol ->>
https://prover.certora.com/output/547/499585e8e92c4538980b7f0d48b528cd?anonymousKey=0730884c87d843db86f6027ce846e67062a93da2

[Czar102]

This looks valid, but the BordaNewBug.sol seems to fail the rule from #4

[1nc0gn170]

Ah thats probably because, the rule which is failing is added by you in Broda.spec?

[Czar102]

I am trying to help. Every submission needs "reports of all previously acknowledged bounty specs on BordaNewBug.sol", which this was lacking. #4 was submitted earlier than this issue/pr.

From my understanding, this should be valid if #4 is considered invalid.

[nd-certora]

#4 is considered acknowledged as missing spec, therefore since this is the same conceptual bug it is not counted. welcome to try more