Uninitialized local variables are documented as a source of a certain type of nondeterminism: http://www.cprover.org/cprover-manual/modeling/nondeterminism/ htt

Uninitialized local variables are documented as a source of a certain type of nondeterminism: http://www.cprover.org/cprover-manual/modeling/nondeterminism/ http://www.cprover.org/cprover-manual/modeling/nondeterminis... So the checker treats them as defined, but with an unknown variable. You could have written this instead: extern int unknown_int_value(void); int x = unknown_int_value(); And leaving unknown_int_value undefined (so it's not visible to the analyzer). Or write a function and use x as a parameter. I suspect CBMC does this to have a convenient syntax for this frequent scenario. Apparently, it's used quite often, as in these examples: https://model-checking.github.io/cbmc-training/cbmc/overview/proof.html https://model-checking.github.io/cbmc-training/cbmc/overview... It seems that CBMC is not intended to check production sources directly against C semantics, but to prove things about programs written in a C-like syntax.