By the way, with the --flow-debug switch [1] I get the same output (besides the error) when the exit is present and when not, so it doesn’t give a clue about why it is coming to that conclusion.
[1] See output in How does `gnatprove --flow-debug` use graphviz?