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