Incorrect result from Certora

[shikhar229169]

As Patrick mentioned in the example for FormalVerificationCatches with Certora it produces the correct revert answer but with wrong reasons.
But this would lead to inconsistencies in result provided as it would havoc a variable on its own and will be producing incorrect revert answer and this would be very tedious to work upon in a complex function as the reverted answer provided was actually incorrect.

The same case happened when I run Certora on the same function where it produced 105 as the revert answer instead of 99.
https://prover.certora.com/output/740813/6a1ce28f006e4e1b86f0cccdbdd6e526?anonymousKey=e7ff49a67aa8bc78f9360cfb8e158f33d5296b41

Is there any fix for this?

[EngrPips]

Hello @shikhar229169, I don't work with Certora as I prefer Halmos because of its simplicity. I am not sure if there is a fix for that problem as Patrick didn't mention one in the course.

[shikhar229169]

I got the fix, it was ahead in the lesson.

[EngrPips]

Interesting. I didn't pay too much attention to the Certora parts of the course since I had already chosen Halmos. Keep crushing it.