Kodkod natively supports (at least) two's complement add/sub/mul/div/remainder
by constructing the typical circuit that performs the operation.
For add/sub, the circuit is linear in bitwidth.
For mul/div/rem, the circuit is exponential in bitwidth I believe (I could be wrong).

Now, what Alloy Analyzer does is when it sees you import util/integer
and you call its add/sub/mul/div/rem function, then instead of generating
a list of constraints that imply add/sub/mul/div/rem, it simply inlines the circuit
generated by Kodkod.