; lambda40 :: SInteger
(define-fun lambda40 () Int
  0)