goto-cc
cbmc