#include <w32k.h>

#define NDEBUG
#include <debug.h>