Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Do not turn trivially diverging loops into assume(false) (#3223)
CBMC's symbolic execution by default turns `while(true) {}` loops into `assume(false)` to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops. Resolves: #2909
- Loading branch information