alloy2/models/bugs/bug_C0skd
