Weird behavior if WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException #850
Description
If WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException for some subset of the worker threads,
- a stack trace is printed but Silicon does not crash completely
- for some reason onStart is executed for only two workers max (???)
- sometimes Silicon hangs forever
- sometimes it still reports results (unclear if all results or some subset)
Immediate question:
Can a crash like this lead to successful verification even though there should be errors, i.e., is this a potential unsoundness, or is it just weird? And does this change is branch parallelization is on?
Also, does the type of exception matter?