Lattice INT_TOP ⊤ :int INT_MIN -n INT_TOP->INT_MIN INT_MINDOTS ... INT_TOP->INT_MINDOTS INT_MINUS -1 INT_TOP->INT_MINUS INT_ZERO 0 INT_TOP->INT_ZERO INT_PLUS 1 INT_TOP->INT_PLUS INT_MAXDOTS ... INT_TOP->INT_MAXDOTS INT_MAX +n INT_TOP->INT_MAX INT_BOT ⊥ :int INT_MIN->INT_BOT INT_MINDOTS->INT_BOT INT_MINUS->INT_BOT INT_ZERO->INT_BOT INT_PLUS->INT_BOT INT_MAXDOTS->INT_BOT INT_MAX->INT_BOT