team-worthwhile/worthwhile — Issue #74: When loop condition + invariant is verified, the whole loop is marked in the UI
Author: jspam
Created: 2012-02-19 13:58:36+00:00
State: open
Labels: ui

The prover reports its verification result of "loop condition and invariant imply block postcondition" with the ```statement``` parameter set to the loop. Thus, in the UI, the whole loop is marked, which a) does not look pretty and b) covers other markers in the loop, e.g. invariant markers.