Try to enable cpa.smg.handleUnknownDereferenceAsSafe=false for CPAchecker SMG
Currently CPAchecker does not immediately fail when it encounters dereferences of unknown pointers. In some cases it can result in weird false alarms later and much efforts may be necessary to find root causes. In case of that option CPAchecker should report unsafes earlier and they should be clearer. Unfortunately, there may be too many unsafes demonstrating a lot of blanks in the environment (model).