CBMC replaces array copy by a built-in statement array_copy or array_replace. 2LS currently doesn't support these, which makes analysis of programs using such operations fail.
Usage of the mentioned operations is currently disabled in competition mode by local_SSAt::disable_unsupported_instructions.
CBMC replaces array copy by a built-in statement
array_copyorarray_replace. 2LS currently doesn't support these, which makes analysis of programs using such operations fail.Usage of the mentioned operations is currently disabled in competition mode by
local_SSAt::disable_unsupported_instructions.