Interpreter throws ugly error message when prover is missing

[leonhandreke]

[FRONDS]

Seems to be done already by a friendly spirit or something.

[jspam]

Then why don’t you close the issue?

[jspam]

Well, the spirit seems to have been not so friendly, because this persists: I get an "unknown validity" interpreter error (without indication of what went wrong) plus the following on the console:

java.io.IOException: Cannot run program "z3bla": java.io.IOException: error=2, Datei oder Verzeichnis nicht gefunden
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:475)
    at edu.kit.iti.formal.pse.worthwhile.prover.StdProver.checkFormula(StdProver.java:69)
    at edu.kit.iti.formal.pse.worthwhile.prover.Z3Prover.checkFormula(Z3Prover.java:1)
    at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker$1ProverCallerTask.call(SpecificationChecker.java:269)
    at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker$1ProverCallerTask.call(SpecificationChecker.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:334)
    at java.util.concurrent.FutureTask.run(FutureTask.java:166)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1110)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:603)
    at java.lang.Thread.run(Thread.java:679)
Caused by: java.io.IOException: java.io.IOException: error=2, Datei oder Verzeichnis nicht gefunden
    at java.lang.UNIXProcess.<init>(UNIXProcess.java:164)
    at java.lang.ProcessImpl.start(ProcessImpl.java:81)
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:468)
    ... 9 more

Although judging by the stack trace this might be the prover's fault after all -- what do you think, @bafain & @leonhandreke ?

[leonhandreke]

Nope, this really isn't my problem. The prover makes a ProverResult with the output available, use it wisely!