INPUTS
  s0 :: SArray Word32 Word32, aliasing "a"
  s1 :: SWord32, aliasing "x"
  s2 :: SWord32, aliasing "y"
CONSTANTS
  s3 = 2 :: Word32
  s6 = 3 :: Word32
  s12 = 1 :: Word32
TABLES
UNINTERPRETED CONSTANTS
  [uninterpreted] f :: (True,Nothing,SWord32 -> SWord64)
USER GIVEN CODE SEGMENTS
AXIOMS-DEFINITIONS
DEFINE
  s4 :: SWord32 = s1 + s3
  s5 :: SBool = s2 == s4
  s7 :: SArray Word32 Word32 = store s0 s1 s6
  s8 :: SWord32 = s2 - s3
  s9 :: SWord32 = select s7 s8
  s10 :: SWord64 = [uninterpreted] f s9
  s11 :: SWord32 = s2 - s1
  s13 :: SWord32 = s11 + s12
  s14 :: SWord64 = [uninterpreted] f s13
  s15 :: SBool = s10 == s14
  s16 :: SBool = s5 => s15
CONSTRAINTS
ASSERTIONS
OUTPUTS
  s16