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