Link to PR : https://github.com/Certora/tutorials-code/pull/9 A run of the new `BordaMissingRule.spec` on `Borda.sol ` https://prover.certora.com/output/95406/ad390610904f490fb14c8a39d244a929?anonymousKey=8da1cada70decf9448a2a7fad759cf69e3fdb464 A run on the `Borda.spec` on `BordaNewBug.sol` https://prover.certora.com/output/95406/a94453aaf96f40cab8c20bb9ca1a208f?anonymousKey=55dfe859583816dabe226c6f105bcba758a2fd9c A run on the `BordaMissingRule.spec` on `BordaNewBug.sol` https://prover.certora.com/output/95406/cf90c05695cd4c9a8f01da8ac2cb5e22?anonymousKey=9ffe665d58643a3ad573d1b73f3e7b118f82de13
Activity
nd-certora commentedon Sep 28, 2023
This is not acknowledged as there is no effect on the winner from the point of view of the IBorda interface . If you could have:
It would have been caught by the existing spec. you are welcome to try more if there are still no five acknowledged