Klever

In branch mav this issue was also revealed.
In order to solve it the following steps were taken:
1. All error traces are printed immediately after they have been found by CPAchecker by means of specific option (cpa.arg.errorPath.exportImmediately=true). By default all found error traces are printed in the coarse of printing all statistics, which may take a lot of time. In case of specifying the suggested option error traces will be printed before that part.
2. Recommendation. It is suggested to use "soft" and "hard" time limits in CPAchecker, so the verifier get time to print statistics. Currently in klever configuration only "hard" time limit can be specified (in ms):
"resource limits": {
"CPU time": 1000000...
In order to specify "soft" time limit one can use option in CPAchecker (limits.time.cpu=900s).
3. Do not correct the Unknown verdict into the Unsafe verdict in case of finding an error trace unless multiple error analysis was specified.
4. But this problem may take place even in multiple error analysis (for example, the last found error trace was about 1Gb and could not be printed in 100s). In order to solve this a new try block was added to intercept such exceptions and output warnings for such traces without further processing them.

As I understand, this issue will be resolved in master as soon as the branch mav will be merged.

BTW, I have used that option and it also didn't help.

Specifying soft time limits will not always help as well as you pointed out. It will just help to get more complete logs. Just in case of finding several bugs it can help a bit.

Catching and ignoring exceptions when parsing error traces is very bad since you will miss important issues one day.

You suggested the proper solution: when we don't try to find multiple error traces then parse error traces just in case of the verification status is Unsafe (as it was before).

But note that this status is likely specified by the BenchExec wrapper around CPAchecker on the basis of its log (examine source code). And this should be done when one tries to find multiple bugs. You should specify a special verification status if the overall status is Unknown, e.g. Incomplete Unsafe and specify in it the number of successfully printed error traces (it should be calculated on the basis of logs).

Catching and ignoring exceptions is proposed to use for MEA only, because there are examples of very big and useless error traces.
If we do not use option for MEA and got incomplete trace for any reason, then VTG most likely should fail.

I understood that well, but this a dirty workaround. One shouldn't understand what error traces weren't outputted successfully on the basis of exceptions during their parsing.

Please, discuss with Philipp, how to properly update the CPAchecker tool info in BenchExec to meet multiple error traces well. I am sure that he will veru glad if you will implement everything required by yourself.

BTW, here is the place in the CPAchecker tool info where they understand that the final verdict is Unsafe that corresponds to the only properly printed error trace (witness). You need to do something like that for several error traces perhaps when the final verdict is Unknown, e.g. due to resource limits.

From 036a882 when several witnesses are found but some of them aren't printed successfully and the final verdict is Unknown there will be the exception like in the issue description.

Pavel is also interested in the proper decision of this issue since his analysis always finds for many bugs by its nature.

I hope that you clearly understand that we will not use a fork of BenchExec like we used a fork of CPAchecker with MAV for some time. Just when the community will agree with your improvements and they will be in BenchExec master, we will start review of your related changes in Klever. This is a very nice filter, isn't it?

Yes, I am going to wait for a new version of BenchExec, which also make implementation in our system much more easier.

we will start review of your related changes in Klever

If you are going to review it, please, read at least my documentation first.

Evgeny Novikov wrote:

This is a very nice filter, isn't it?

It is not nice for our system, that I will have to reimplement the same method second time, which was not changed in a few years, instead of doing something more important (for example, improve methods or their implementations or even suggest some new methods).

After discussion it was decided, that BenchExec does not require specific changes to support MEA, because such changes are pretty minor and can be (and should be) implemented in our system (for example, what the point of adding in general tool -- BenchExec -- list of found witnesses if we can search in output directory by the same pattern).

The real change, which should be done in MEA implementation, is to add support for any verifier, which can be used in BenchExec. In particular, the way of determine Unsafe-incomplete verdict should be generalized. This task is related to issue #7800.

Therefore, I suggest the following schema:
1. Refactor all strategies (as they are in master) according to #7800, so they could operate (or fail if not supported) with any verifier.
2. Reimplement MEA method (by generalizing implementation in master).
3. Step-by-step refactor each strategy in master in accordance with their correct implementation in branch "new_format_of_strategies".
4. Merge this in master without waiting for review from those, who completely do not accept ideas of this method.

If there will be problems with merge again, it all will be a waste of resources and it is better to ignore this issue. It is enough that this year I had to reimplement the same methods twice, because they were not merged in time, since reviewer simply did not accept ideas of methods for some unknown reasons, instead of improving them. Maybe we need different reviewers for different components for better development of our system.