CBMC version: 6.2.0
Operating system: macOS

CBMC crashes if the __CPROVER_loop_entry() contract is used inside a __CPROVER_assert()
contract that is within a loop body.

Is this usage legal or not? It should either work, or should result in a clear error message.

Example code to follow.