; -- user given definition: lambda40
(define-fun lambda40 () Int
  0)