Currently, escaped locals (pointer was saved into globals) are not correctly passed to callees, as enter filters via Basetype.Variables.is_global k instead of is_global (Analyses.ask_of_ctx ctx) k.

Looking up the corresponding value in the local state then leads to bot, which is ignored when merging over all possible addresses that a pointer may point to.

Minimal example:

#include <assert.h>
int* ptr;
int nine = 9;

int other() {
    assert(*ptr == 8); //UNKNOWN!
}

int main()
{
    int g = 8;
    int top;

    if(top) {
        ptr = &g;
    } else {
        ptr = &nine;
    }

    other();
}

TODO: Investigate if this fixes the unsoundnesses for SV-Comp.