Currently CIL removes empty if statements like

if (x) {
}

For Goblint's use case there are two reasons to keep them, just like we prevent removal of other kinds of branching from the CFG:

1. We are unsound by missing races to variables in the conditional expression

   #include <pthread.h>
   #include <stdio.h>
   
   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);
     if (myglobal) { // RACE!
   
     }
     pthread_mutex_unlock(&mutex1);
     return NULL;
   }
   
   int main(void) {
     pthread_t id;
     pthread_create(&id, NULL, t_fun, NULL);
     pthread_mutex_lock(&mutex2);
     myglobal=myglobal+1; // RACE!
     pthread_mutex_unlock(&mutex2);
     pthread_join (id, NULL);
     return 0;
   }

2. In automaton witnesses when speaking about branching edges, we should account for all branching edges present in the actual code and not implementation-dependently exclude those which we can syntactically eliminate.