__SD_task_destroy_scheduling_data(task); /* now the scheduling data are not useful anymore */
SD_task_set_state(task, SD_RUNNING);
__SD_task_destroy_scheduling_data(task); /* now the scheduling data are not useful anymore */
SD_task_set_state(task, SD_RUNNING);