In which circumstances one cannot use symbolic execution for assertion checking? To illustrate, take the following example:
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)
Here, we can employ a symbolic execution and find out that ¬A ^ (B < 5) ^ C
violates our assertion. Now, suppose we change the first condition as follows:
if (a){
x = x - 10;
b = b + 5a;
}
With this change, we don't know the new value of x and b. So, can we still use a symbolic execution for assertion checking?
In general, are there any circumstances that we cannot use symbolic execution? i.e., situations where we have to analyze all possible runs of a program.