; -- user given definition: lambda43
(define-fun lambda43 () (_ BitVec 32)
  #x00000000)