NULL is a valid return for malloc. Wouldn’t that case already be handled?

In general, symbolic execution will consider all code paths. If it can't (or doesn't want to) prove that the condition is always true or false it will check that the code is correct in two cases: (1) true branch taken, (2) false branch taken.

There will always be valid programs that are nonetheless rejected by some verifier (Rice's theorem). That is, programs that have really nothing wrong but nonetheless are rejected as invalid

In those cases you generally try to rewrite it in another way

as someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.

I think all paths have to return the same allocation. You would have to solve this in another way.