auf-1.gold

INPUTS
  s0 :: SWord32, aliasing "x"
  s1 :: SWord32, aliasing "y"
  s2 :: SWord32, aliasing "initVal"
CONSTANTS
  s_2 = False
  s_1 = True
  s3 = 2 :: SWord32
  s9 = 3 :: SWord32
  s13 = 1 :: SWord32
TABLES
ARRAYS
UNINTERPRETED CONSTANTS
  [uninterpreted] f :: SWord32 -> SWord64
USER GIVEN CODE SEGMENTS
AXIOMS
DEFINE
  s4 :: SWord32 = s0 + s3
  s5 :: SBool = s1 == s4
  s6 :: SBool = ~ s5
  s7 :: SWord32 = s1 - s3
  s8 :: SBool = s0 == s7
  s10 :: SWord32 = if s8 then s9 else s2
  s11 :: SWord64 = [uninterpreted] f s10
  s12 :: SWord32 = s1 - s0
  s14 :: SWord32 = s12 + s13
  s15 :: SWord64 = [uninterpreted] f s14
  s16 :: SBool = s11 == s15
  s17 :: SBool = s6 | s16
CONSTRAINTS
OUTPUTS
  s17