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