Initializing arrays yields sat with sentinel frontend

[Novak756]

Describe the bug
Including sentinel in the frontend (sea spf,fpf,fcpf) yields sat when trying to intitialize multiple arrays like this:

extern void __VERIFIER_error(void);
extern long __VERIFIER_nondet_long(void);

#define ARRAY_SIZE 32
void init(long* array,int size){
    for(int i = 0; i < size; i++){
    	array[i] = __VERIFIER_nondet_long();
    }
}

int main(){
	long arr_val_87[ARRAY_SIZE];
	init(arr_val_87,ARRAY_SIZE);
	long arr_val_88[ARRAY_SIZE];
	init(arr_val_88,ARRAY_SIZE);
    return 0;
}

To Reproduce
Steps to reproduce the behavior:

1. bug.c = code above
2. sea -m64 spf/fpf/fpcf bug.c

Expected behavior
The program has no assertions so I would expect unsat, not sure what tests sentinel might add that cause this to fail.

Logs, Stacktraces, and Screenshots
Output from running spf with v2 flag

Desktop (please complete the following information):

• OS: Nigthly Docker on Ubuntu 20.14
• LLVM: llvm14
• Z3: 4.8.9 - 64bit

Additional context
Initialising one array is fine, the problem occurs when calling init() on multiple arrays. sea pf and bpf frontends are also ok.
I was trying to explicitly initialize nondet arrays, as unitialized reads are undefined.

[Novak756]

Just realized that adding --inline fixes the issue, so there is probably an issue in the interprocedural analysis.