Open numairmansur opened 7 years ago
What replacing the statement with havoc does is that it flushes the value of the variable. In the example above, the program would be:
procedure foo()
{
var y: int;
var x: int;
var z: int;
x := 7;
x := 7;
assert(x != 7);
}
The error trace will be:
x := 7; x := 7; assume (x = 7)
Output on Ultimate:
[L9] - x := 7;
VAL [x=7]
[L10] * x := 7;
VAL [x=7]
[L11] - assert x != 7;
VAL [x=7]
This is actually a very good example. We see that if we would have replace the second assignment with skip, then the assume statement in the end is not becoming restrictive and hence it would not be marked relevant. Infact none of the two assignments are relevant if we replace them with skip to check there relevance. Replacing the assignment to x with havoc flushes its value and we discover that the value we assign to the variable x is important to reach the error.
Also, if skip were our criteria, then none of the statements in the above program would be relevant.
At least not in the approach with the error invariants.
The above example is not correct.
Integrate the very simple examples we discussed.
Come up with an example in which the error trace already have blockig executions and the replacing the relevant assignemnt with skip
reduces the blocking executions and replacing it with havoc increases it.
Do others also consider assume statements?