This PR proposes to remove the respective dependencies/influences of an unknown from side_dep, side_infl and infl before (instead of in between the recursive calls) of destabilize_with_sides. It would make sure that the same unknown is
always destabilized with the same fuel.
If not, the behavior of restart with fuel is a little unexpected. The fuel could possibly be reduced during the destabilization of side_dep entries and then be less then before when getting back and destabilizing the initial unknown based on entries in infl. This can also leads to a different result when using the CFG comparison. It can be observed in 11-restart/15-mutex-simple-wrap1.c:

int myglobal;
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
  pthread_mutex_lock(&mutex1);
  myglobal=myglobal+1; // RACE!
  pthread_mutex_unlock(&mutex1);
  return NULL;
}

void wrap() {
  pthread_mutex_lock(&mutex2); // changed to &mutex1
  myglobal=myglobal+1; // RACE!
  pthread_mutex_unlock(&mutex2); // changed to &mutex1
}

int main(void) {
  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);
  wrap();
  pthread_join (id, NULL);
  return 0;
}

Since the function wrap is changed and destabilized, one would suspect that 1 fuel is sufficient to restart myglobal (with write-only restarting disabled). Instead the fuel is lost when destabilizing through side_dep in main first and is only 0 when wrap is finally destabilized based on infl. So the race warning is not removed. With the CFG comparison on the other hand, the destabilization immediately starts with the entries in infl (because there are none in side_dep), restarts myglobal because fuel is still 1 and successfully removes the race warning.

I also changed the test case to make them more meaningful with respect to the changes in this PR. It would also fix the open todo in #841.