Incorrect goal location after splitting.
Testcase:
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
When clicking the initially unique goal in the IDE, both calls bar x
are properly highlighted as being the preconditions to prove. After splitting the goal, both goals cause the IDE to highlight the first call bar x
, while the second goal is meant to be the precondition of the second call.
Note that this happens quite often in practice. For example, the fast exponentiation algorithm (or its variant, the ancient Egyptian multiplication) contains both divisions and modulos, which all have the same precondition, so all the goals point to the same location of the code.