INPUTS s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS s_2 = False s_1 = True s2 = 1 :: SWord8 TABLES ARRAYS UNINTERPRETED CONSTANTS AXIOMS DEFINE s3 :: SWord8 = s0 + s2 OUTPUTS s3