Field of dynamic objects in a condition fixes the value of all fields

[viktormalik]

For example, in the following program:

Node *list = NULL;
while (__VERIFIER_nondet_int())
{
// create a node
Node *x = malloc(sizeof(*x));
    x->data = __VERIFIER_nondet_int() ? 1 : 0;
    x->next = list;
    list = x;
}

while (list != NULL && list->data == 0)
{
    list = list->next;
}

if (list)
    assert(list->data == 1);

list->data is used in the second loop condition. After transforming to the SSA form, dynamic_object$28.data != 0 holds for the rest of the program (after the 2nd loop), which causes the assertion to be wrongly evaluated as true.

[viktormalik]

My mistake, the given program is indeed correct. If we replace the last if by a while, then we could again get to a node with value 0, but thanks to splitting of dynamic objects, there is no true positive.