Rule: SPEC/T9509 foo1 @Int
    Rule: SPEC/T9509 foo1 @Int