definition module set_return_code;

:: *UniqueWorld :== World;
set_return_code :: !Int !UniqueWorld -> UniqueWorld;
// void set_return_code (int return_code);