int bug521c_beforeupcrelaxed;
#include <upc_relaxed.h>
int bug521c_afterupcrelaxed;

int bug521c_beforebug521h;
#include <bug521.h>
int bug521c_afterbug521h;

int main() {
  return 0;
}