В каких обстоятельствах мы не можем использовать символическое исполнение?

Question

В каких обстоятельствах нельзя использовать символическое выполнение для проверки утверждения? Для иллюстрации возьмем следующий пример:

      int a = A, b = B, c = C; \\symbolic

int x = 0, y = 0, z = 0;
if (a){
  x = -2
}
if (b < 5){
  if (!a && c) {y = 1;}
  z = 2;
}
assert (x + y + z != 3)

Здесь мы можем использовать символическое исполнение и выяснить, что нарушает наше утверждение. Теперь предположим, что мы изменили первое условие следующим образом:

      if (a){
  x = x - 10;
  b = b + 5a;
}

С этим изменением мы не знаем нового значения x и b. Итак, можем ли мы по-прежнему использовать символическое выполнение для проверки утверждений?

В общем, есть ли обстоятельства, при которых мы не можем использовать символическое исполнение? то есть ситуации, когда мы должны проанализировать все возможные запуски программы.