CBMC version: 516f109218a522bf33ade14e3e20003c1427beb0 Forking off from @martin-cs's recent comment: https://github.com/diffblue/cbmc/pull/6249#discussion_r754508259 We use the `throw 0` at several places throughout code base. We should use audit these instances and: 1. check if it would be more appropriate to raise an `INVARIANT` violation, 2. throw `exception`s or at least `std::string`s in place of `0`