Closed
Description
See https://github.com/diffblue/cbmc/blob/develop/src/cbmc/bmc.cpp#L562 and https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/unwind.cpp#L53. The former is better but is specific to BMC, the latter includes comparisons to signed -1 instead of std::numeric_limits::max
. As a result another duplicate has been made in https://github.com/diffblue/test-gen/pull/1236 which should be moved somewhere in CBMC and used by the existing two implementations.
Metadata
Metadata
Assignees
Labels
No labels