assertion - 在哪些情况下我们不能使用符号执行？

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)

在这里，我们可以使用符号执行并找出¬A ^ (B < 5) ^ C违反我们的断言。现在，假设我们将第一个条件更改如下：

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

通过这种变化，我们不知道 x 和 b 的新值。那么，我们仍然可以使用符号执行来进行断言检查吗？

一般来说，有什么情况我们不能使用符号执行？即，我们必须分析程序所有可能运行的情况。