>> ()
{
  <expect> max ERR_PARAMETER "when x < 0" () {
                                               dword x = 2^32;
                                               dword y = 1;

                                               z = max (x, y);
                                             };

  <expect> max ERR_PARAMETER "when y < 0" () {
                                               dword x = 1;
                                               dword y = 2^32;

                                               z = max (x, y);
                                             };
  ú
  ú
  ú
}