Hello @starkos
Sorry for the delay, this issue looks simple but hides a great complexity, it’s not easy to give a clear answer.
The good news is that I managed to reproduce the issue, thanks to your great reproducer. Indeed, the engine does not support correctly such kind of user-defined preconditions in another file. I therefore created a ticket to track it: SONARJAVA-4026.
The “bad” one is that it is unclear how to solve this issue, improving the symbolic execution engine is something we have on the table, but I don’t expect it to be fixed in the near future…
At this point, the best I can suggest is to use well-known preconditions, like java.util.Objects.requireNonNull, performing the same. This one is correctly supported by the engine.
Hope it clarifies the situtation.
Quentin