INPUTS s0 :: SWord8, aliasing "x" CONSTANTS s_2 = False s_1 = True TABLES ARRAYS UNINTERPRETED CONSTANTS USER GIVEN CODE SEGMENTS AXIOMS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s1 * s1 CONSTRAINTS OUTPUTS s2