There's one important point that I was reminded of but didn't get around to checking myself yet: the tool version lookup in BenchExec will now invoke ./goblint_runner.py --version. So that must still work. It should probably just delegate to goblint --version, because the runner script is in the same repository and doesn't need a separate version from Goblint itself.
Notably, we should avoid that the version lookup ends up doing the version lookup repeatedly in sequential portfolio...

There's one important point that I was reminded of but didn't get around to checking myself yet: the tool version lookup in BenchExec will now invoke ./goblint_runner.py --version. So that must still work. It should probably just delegate to goblint --version, because the runner script is in the same repository and doesn't need a separate version from Goblint itself. Notably, we should avoid that the version lookup ends up doing the version lookup repeatedly in sequential portfolio...

In case that there is no portfolio-config present, the runner just forwards everything as is to ./goblint. I also tested this a minute ago, and it works.

There's one important point that I was reminded of but didn't get around to checking myself yet: the tool version lookup in BenchExec will now invoke ./goblint_runner.py --version. So that must still work. It should probably just delegate to goblint --version, because the runner script is in the same repository and doesn't need a separate version from Goblint itself. Notably, we should avoid that the version lookup ends up doing the version lookup repeatedly in sequential portfolio...

If I remember correctly, this is already accounted for.
@DrMichaelPetter : You wanted to make a sanity check run, did you get to it already?

@DrMichaelPetter : You wanted to make a sanity check run, did you get to it already?

So is there something still being done? If not, then I would merge this and integrate it into a new SV-COMP artifact.

Yesterday, @arkocal and @DrMichaelPetter had a discussion whether the behavior of BenchExec w.r.t. reading out a verdict is defined in case multiple verdicts are in the output.

As I understand, currently, this script might produce output containing multiple Unknown verdicts, and finally some true verdict, in case the last configuration can prove safety of a task.
The question is whether it is defined for BenchExec to behave in the intended way for such output, i.e., to accept the final true verdict.

Anyways, since this currently works, this may not be a blocker.

How multiple verdicts are treated is determined by our tool-info module in BenchExec here: https://github.com/sosy-lab/benchexec/blob/ecc0f2cec0095c80684037b2b3f875d508571960/benchexec/tools/goblint.py#L89-L116.
I also wondered about this earlier and checked: the loop over all output lines will just override the previous one if a new match is found, so it should all work.