René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Forbid view function reverts","articleBody":"Hi, displaying info below:\r\n\r\npr: #16 \r\n\r\nA run of the new `BordaMissingRule.spec` on the original [`Borda.sol`](https://github.com/Certora/tutorials-code/blob/master/lesson3_violations/Borda/Borda.sol) that is verified is [here](https://prover.certora.com/output/2949/4a009af4eb98473fb104841ef9fed7c9?anonymousKey=bc3dd6b5ace4b4e3a73efadc40d3a5dba6f83a0e)\r\n\r\nA run of [`Borda.spec`](https://github.com/Certora/tutorials-code/blob/master/lesson3_violations/Borda/Borda.spec) on `BordaNewBug.sol` showing the existing spec misses the bug is [here](https://prover.certora.com/output/2949/edc685803a4d41eb8e789263a71df2c4?anonymousKey=2c22a59bd9fbc202af4da13624d5e2e66af1088b)\r\n\r\nReports of all previously acknowledged bounty specs on `BordaNewBug.sol`: included in the above verification, see `votedFunctionIsVotedMapping`, `preferLastVotedHigh` and `onlyVotingCanChangeTheWinner`.\r\n\r\nA run of `BordaMissingRule.spec` on `BordaNewBug.sol` showing your rule catches the bug is [here](https://prover.certora.com/output/2949/657b1981ebe54939b1c515bee8f211a3?anonymousKey=fec4b9c6ccd968f4f58832c3b1576b480f8e5f7b)\r\n\r\nThanks for the challenge yet again!","author":{"url":"https://github.com/Czar102","@type":"Person","name":"Czar102"},"datePublished":"2023-09-28T11:35:41.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":1},"url":"https://github.com/17/tutorials-code/issues/17"}