INPUTS
  s0 :: SWord8, aliasing "x"
  s1 :: SWord8, aliasing "q"
CONSTANTS
TABLES
ARRAYS
UNINTERPRETED CONSTANTS
USER GIVEN CODE SEGMENTS
AXIOMS
DEFINE
  s2 :: SWord8 = s0 + s0
  s3 :: SWord8 = s0 - s0
  s4 :: SWord8 = s2 * s3
CONSTRAINTS
ASSERTIONS
OUTPUTS
  s1
  s4