; lambda43 :: SWord32
(define-fun lambda43 () (_ BitVec 32)
  #x00000000)