Open
Description
CBMC version: 5.67.0
Operating system: N/A
We need to give the proof writer more help understanding why an ensures clause is failing by providing a bit of a trace of the expression evaluation.
If you open viewer to look at a failure trace for an ensures clause failure, all you get is a single line saying failure. In contrast, if you define a function predicate and look at its evaluation in viewer, you see a step-by-step description on how the predicate was evaluated. At the very least you see the values assigned to formal arguments. Can we do the same thing for expressions in assign clauses? At the very least, see the values being used for the variables appearing in the expression?