Function smallvec_array_size 

pub uninterp spec fn smallvec_array_size<A>() -> nat

The element count that A’s smallvec Array impl reports (A::size()). Bound-free on purpose: smallvec implements Array for [T; N] only for a fixed list of lengths (its const_generics feature is off), so an Array bound would make [T; N] with generic N fail to typecheck (E0277), and the size mirror below could not be stated for every N.