Bug in contract replacement with conditional assings clauses

[feliperodri]

CBMC version: 5.69.1 (cbmc-5.59.0-676-gb4a4122dee)
Operating system: N/A
Exact command line resulting in the issue:

goto-cc main.c -o main.goto
goto-instrument --dfcc main --enforce-contract bar --replace-call-with-contract foo main.goto main-mod.goto
cbmc main-mod.goto --pointer-check

What behaviour did you expect: No failures.
What happened instead: NULL pointer derefecences.

#include<stdlib.h>

void foo(int *out)
__CPROVER_requires(out == NULL || __CPROVER_is_fresh(out, sizeof(*out)))
__CPROVER_assigns(out != NULL : *out)
{
    if(out)
        *out = 1;
}

void bar()
{
    foo(NULL);
}

int main(void)
{
    bar();
}

[remi-delmas-3000]

fixed by #7380