# include "basic.h"
# include "randomNumbers.h"
/*@constant null ghbucket ghbucket_undefined; @*/
# define ghbucket_undefined 0
# include "basic.h"
# include "randomNumbers.h"
/*@constant null ghbucket ghbucket_undefined; @*/
# define ghbucket_undefined 0