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 の新しい値はわかりません。では、アサーション チェックにシンボリック実行を引き続き使用できますか?

一般的に、シンボリック実行を使用できない状況はありますか? つまり、プログラムの可能なすべての実行を分析しなければならない状況です。