      subroutine cbmc
      return
      end
