void r250_init(int seed);
unsigned long r250(void);
double dr250(void);