INPUTS
  s0 :: SWord8, aliasing "x"
CONSTANTS
TABLES
ARRAYS
UNINTERPRETED CONSTANTS
USER GIVEN CODE SEGMENTS
AXIOMS
DEFINE
CONSTRAINTS
ASSERTIONS
OUTPUTS