Z3::IntExpr

Returns true if this object is not equal to other.

By default this method is implemented as !(self == other) so there's no need to override this unless there's a more efficient way to do it.

It doesn't match Crystal on a negative right side, but nobody does modulo a negative anyway, and the Python Z3 API does the same thing

Returns false (other can only be a Value here).

Z3 spells this the other way round, as "other divides self"

Whether this is the same term as other. Z3 hash-conses its expressions, so this is structural equality - Z3.int("a") + 1 built twice is one term. It is a named method rather than == because == builds a Z3 expression instead of answering a Crystal Bool - see the Limitations section of the README.

Takes the low n bits, so it wraps rather than failing on values which don't fit - Z3.int("a").to_bv(8) of 256 is 0. Which Integer comes back out depends on how you read it again: BitvecExpr#signed_value or #unsigned_value.

Every sort which can hand back a Crystal object spells it #value. Z3 Ints are unbounded, so this is a BigInt - #to_i is the Int32 one, as everywhere else in Crystal.