Pulse not interpreting _fun___get_array_length() correctly

[matjin]

For the following code:

    static void expectNoError() throws IOException {
        String[] paths = new String[5];
        if (paths.length < 5) {
            Object x = null;
            x.hashCode();
        }
    }       

We expect Pulse to determine that the path in which the nullptr dereference might occur is not satisfiable. However, it reports the null dereference. I'm attaching the complete debug output to this post for ease of explanation. infer-out.tar.gz