Dafny should exit nonzero when Z3 can't be run

[mattmccutchen-amazon]

Dafny version

master (b956d23)

Code to produce this issue

method Test1() { assert true; }

Command to run and resulting output

Attempting to use z3-4.12.1-x64-glibc-2.35 on a system with an old glibc (like one I'm using at Amazon):

% PATH=REDACTED/z3-4.12.1-x64-glibc-2.35/bin:$PATH REDACTED/Scripts/dafny /compile:0 trivial.dfy; echo $?
Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libc.so.6: version `GLIBC_2.34' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libc.so.6: version `GLIBC_2.32' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libc.so.6: version `GLIBC_2.33' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libstdc++.so.6: version `GLIBCXX_3.4.30' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libstdc++.so.6: version `GLIBCXX_3.4.29' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libstdc++.so.6: version `GLIBCXX_3.4.26' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Prover error: REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by REDACTED/z3-4.12.1-x64-glibc-2.35/bin/z3)

Advisory: Test1 (correctness) SKIPPED due to I/O exception: Broken pipe
/local/home/matmccut/dafny/dafny-tests/trivial.dfy(1,7): Verification encountered solver exception (Test1 (correctness))

Dafny program verifier finished with 0 verified, 0 errors, 1 solver exceptions
0

What happened?

The exit code is 0, as seen on the last line of the output, even though the input program has not been verified at all. It should be nonzero so that a script running Dafny will know that something went wrong.

I noticed this in the case where Z3 cannot be run because of broken shared library dependencies. Under some conditions, a failure to run Z3 causes a hang (#2370); under other conditions, it just causes a "solver exception" without a hang. I don't know whether the same problem occurs with other kinds of "solver exceptions".

What type of operating system are you experiencing the problem on?

Linux