Primitive Type Casting: C/C++ allows you to cast between totally unrelated types. This can be problematic for model checking. Avoid type casting between unrelated types and in particular primitive
types. For example,
Casting between unrelated types requires overhead for keeping values consistent. For primitive types, this also requires creating objects instead of primitives and explicit modeling of the memory and the platform. In languages like Java you cannot even use the immutable standard box types like java.lang.Integer. Furthermore, operations on the primitives have to be turned from direct bytecode instructions into method calls, creating more overhead.