Prevent Boogie from hanging

[keyboardDrummer]

Prevent Boogie from hanging when an exception occurs when acquiring a checker, which can occur of the solver path is incorrect or the solver doesn't function correctly

[atomb]

Thanks for fixing this!

[shazqadeer]

@keyboardDrummer : This test does not pass on my Mac laptop. Here is the output:

shaz@shaz-mbp commandline % lit broken_solver_more_impls_than_cores.bpl -vv
lit: /Users/shaz/Source/boogie/Test/lit.site.cfg:13: note: using Python 3.7.5 (default, Oct 22 2019, 10:35:10) 
[Clang 10.0.1 (clang-1001.0.46.4)]
lit: /Users/shaz/Source/boogie/Test/lit.site.cfg:78: note: Repository root is /Users/shaz/Source/boogie
lit: /Users/shaz/Source/boogie/Test/lit.site.cfg:111: note: Using Boogie: dotnet /Users/shaz/Source/boogie/Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll -useBaseNameForFileName
lit: /Users/shaz/Source/boogie/Test/lit.site.cfg:128: note: Using diff tool: /usr/bin/diff --unified=3 --strip-trailing-cr --ignore-all-space
-- Testing: 1 tests, 1 workers --
FAIL: Boogie :: commandline/broken_solver_more_impls_than_cores.bpl (1 of 1)
******************** TEST 'Boogie :: commandline/broken_solver_more_impls_than_cores.bpl' FAILED ********************
Script:
--
: 'RUN: at line 1';   ! dotnet /Users/shaz/Source/boogie/Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll -useBaseNameForFileName /vcsCores:1 "/proverOpt:PROVER_PATH=doesNotExit" "/Users/shaz/Source/boogie/Test/commandline/broken_solver_more_impls_than_cores.bpl" > "/Users/shaz/Source/boogie/Test/commandline/Output/broken_solver_more_impls_than_cores.bpl.tmp"
: 'RUN: at line 2';   /usr/bin/diff --unified=3 --strip-trailing-cr --ignore-all-space "/Users/shaz/Source/boogie/Test/commandline/broken_solver_more_impls_than_cores.bpl.expect" "/Users/shaz/Source/boogie/Test/commandline/Output/broken_solver_more_impls_than_cores.bpl.tmp"
--
Exit Code: 127

Command Output (stdout):
--
$ ":" "RUN: at line 1"
$ "!" "dotnet" "/Users/shaz/Source/boogie/Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll" "-useBaseNameForFileName" "/vcsCores:1" "/proverOpt:PROVER_PATH=doesNotExit" "/Users/shaz/Source/boogie/Test/commandline/broken_solver_more_impls_than_cores.bpl"
# command stderr:
'!': command not found
error: command failed with exit status: 127

--

********************
********************
Failed Tests (1):
  Boogie :: commandline/broken_solver_more_impls_than_cores.bpl


Testing Time: 0.11s
  Failed: 1

Why is the name of the test not simply "broken_solver.bpl"? As far as I can tell, the output of the test is just due to the missing solver.

[keyboardDrummer]

@shazqadeer maybe it's a difference in the version of lit we're using. I'm using 16.0.0. Here's a fix: #720

Why is the name of the test not simply "broken_solver.bpl"? As far as I can tell, the output of the test is just due to the missing solver.

Without this PR, the test would hang but only if you have fewer solvers than implementations.