/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md File Reference