[CI] Download, unpack solver and test solver on dumb test file

[bobot]

No description provided.

[bobot]

@martinjonas Currently it is executing the solver using subprocess.run but in the docker of the cluster, do you think we can execute it really as it will be executed in the cluster?

[martinjonas]

@martinjonas Currently it is executing the solver using subprocess.run but in the docker of the cluster, do you think we can execute it really as it will be executed in the cluster?

Not exactly as it will be executed in the cluster (VerifierCloud is not public yet), but we can certainly execute it via BenchExec, but locally. This should be almost the same as in the cluster. Or, taking one more step back, we can execute it using runexec (https://github.com/sosy-lab/benchexec/blob/main/doc/runexec.md), which is the program that is used by BenchExec to execute the solvers and which takes care of isolation, resource limits and resource measurement.

But I am not sure whether the change is worth it. If the solver can be executed in the docker container, it is very likely that it can be executed also using BenchExec (if our BenchExec configuration files are correct).

[bobot]

runexec can even be used through API, https://github.com/sosy-lab/benchexec/blob/6467aa5e1117155586f50928c17097fa87f341de/doc/runexec.md?plain=1#L77 . The advantage is to also be able to parse the output like benchexec will do it. So we can really check that the solver answer sat (as parsed by benchexec) on trivial sat examples.

[bobot]

benchexec and runexecutor are not installed in the image, so we will parse normally.