Report NotAnalyzedResult instead of UnprovableResult when analysis stops early

[schuessf]

Currently, if a specification is not analyzed (e.g., because an error was found earlier and Stop after first violation was found is enabled), Ultimate reports a UnprovableResult for the remaining specifications. This is misleading, since it can look like we failed to verify those specifications, when in fact they were never checked.

This PR introduces a dedicated NotAnalyzedResult for such cases (as already proposed by @danieldietsch here 😉), which should make the results easier to understand (e.g., in the web interface). As a result, the output changes from

- UnprovableResult [Line: ...]: Unable to prove that a call to reach_error is unreachable
  Unable to prove that a call to reach_error is unreachable
  Reason: Not analyzed. 

to

- NotAnalyzedResult [Line: ...]: Not analyzed if a call to reach_error is unreachable
  Not analyzed if a call to reach_error is unreachable

As a potential follow-up (not yet done in this PR), we could also add a setting whether such results should be output at all.

[maul-esel]

👍 good, I've been meaning to do something about that.

Beyond the confusing message, the sheer number of these results often makes it difficult to find the actually meaningful information. Would it be an option to summarize them in one result? (either now, or with a future PR that introduces a setting)

[schuessf]

Beyond the confusing message, the sheer number of these results often makes it difficult to find the actually meaningful information. Would it be an option to summarize them in one result? (either now, or with a future PR that introduces a setting)

That would likely require additional changes, since we currently support only a single location (IResultWithLocation). I can see some alternative options that should be easier to integrate:

• Group these into a single result without a location (e.g., "Some specifications were not analyzed"), controlled by a setting (whether we want results for every specification)
• Use the same setting to omit NotAnalyzedResults entirely
• Keep emitting them, but sort results so that NotAnalyzedResults come first and the "important" results appear last