Function ints_need_representation 

pub fn ints_need_representation() -> bool

Whether integers carry a representation choice for the solver being targeted.

SAT has no integers at all: an int variable is encoded as a vector of Booleans, and which encoding it gets is a representation choice like any other. The SMT backend does have integers, but has two ways to express them – linear arithmetic and bit-vectors – so the choice is a representation there too. Minion has one native integer and needs none of this. With no solver family set – a unit test exercising one component, say – integers stay concrete.