alloy2/models/bugs/bug_5Jxa2
