-void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value);
-smx_req_t MC_state_get_executed_request(mc_state_t state, int *value);
-smx_req_t MC_state_get_internal_request(mc_state_t state);
-smx_req_t MC_state_get_request(mc_state_t state, int *value);
+void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
+smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
+smx_simcall_t MC_state_get_internal_request(mc_state_t state);
+smx_simcall_t MC_state_get_request(mc_state_t state, int *value);