All programs verify when SMT solver (Z3) is not present

[rakamaric]

Currently all programs vacuously verify when an SMT solver is not present/installed. Here is the example output when running Corral:

Running corral /local/home/zvorak/smack/src/test/c/basic/a-kem0fn3_.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1 /bopt:proverOpt:O:smt.qi.eager_threshold=100 /bopt:proverOpt:O:smt.arith.solver=2
Corral program verifier version 1.1.8.0
Single threaded program detected
LB: Took 0.00 s
Verifying program while tracking: {assertsPassed}
Error: ProverException: Cannot find any prover executable
Program has no bugs

Boogie verification time: 0.00 s
Time spent reading-writing programs: 0.35 s

Time spent checking a program (1): 0.14 s
Time spent checking a path (0): 0.00 s

Number of procedures inlined: 0
Number of variables tracked: 1
Total Time: 0.9166774 s
Total User CPU time: 1.05 s
SMACK found no errors with unroll bound 1.

We should address this and report an error instead.

[rakamaric]

I would say that this issue is in fact in Corral. Corral reports "Program has no bugs" even when this ProverException is generated. So it should probably be first fixed on the Corral side.