Heap-zones: fixing one variable in a difference row causes the other one to be fixed, too.

[viktormalik]

If one variable is a standalone variable that occurs in a condition of a loop, and the other variable is a field of a dynamic object, values of all fields of all objects represented by the given abstract dynamic objects may be fixed for the rest of the program. For example:

while (nondet && !mark) {
    x = malloc(...);
    mark = nondet ? 1 : 0;
    x->val = mark;
}
assert(head->val == 0)

Since mark occurs in the while condition, SSA contains mark==0 for the code after the loop. Also, heap-zones domain computes dynamic_object$0.val - mark == 0, which causes dynamic_object$0.val to be equal to 0 and the assertion is wrongly evaluated as true.

[viktormalik]

I suggest we check for variables occurring in conditions of loops (or maybe in conditions in general) and then forbid any difference template rows that use such variables with fields of abstract dynamic objects to be used in the rest of the program.

[viktormalik]

@peterschrammel Can you please assign the issue to me? Or you can give me a permission to assign people to issues, so I can do it myself.