Refute: bad framing
This example complains about the body of the `frame_error` method being unreachable due to the fact that its contract is mal-formed.
|Path to example file||refute/frame_error_1.pvl|
|Lines of code||6 lines (comments not included)|
|Lines of specification||1 lines (16.67% of the total)|
|Computation time||17853 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.