DEFINITION MODULE BufBad = Buf(INTEGER);
END BufBad.