Resolve Boogie test deadlocks

[keyboardDrummer]

Changes

• Made a change to the Dispose method of CustomStackSizePoolTaskScheduler.cs, so it now interrupts all its thread instead of joining them. I think this was causing the entire Boogie process to hang after it was finished, causing tests to deadlock.
• Add blame-hang-timeout to the dotnet test invocation that runs the NUnit tests, which allows identifying which test fails when the unit tests timeout.
• Add an undocumented option /processTimeLimit that can be used by tests to let Boogie stop itself after a certain timespan, allowing developers to get a stacktrace of where Boogie was at the point of timeout.
• Remove APIs for cancelling requests, which were only available programmatically and not used by Dafny.
• Fix a bug that could cause a concurrency related exception in QuantifierInstantiationInfo, which was introduced by [Civl] Improvements to pool-based quantifier instantiation #862.
• Use an invariant culture somewhere in printing debug output, so the Boogie tests locally pass on my machine, despite my European culture.
• Some renaming of variations of VerifyImplementation, to make the differences more clear.
• Configure a 30 seconds timelimit per VC for all Boogie tests by default. Added an exception for a few slow tests
• Let Boogie cancel checking of a VC after its timelimit has passed, regardless of what the solver is doing

Testing

• Did not add any additional tests
• Let the test-suite succeed without retries 4 times, in an attempt to determine that it resolves the test instabilities we've had.

[atomb]

This looks like a nice improvement. I saw two tiny things in the tests that might be worth a second look.

[atomb]

Did you mean to check in this file?

[atomb]

It might be worth having a process time limit here, too, since there's no strict guarantee that Z3 will ever terminate given a resource limit.

[shazqadeer]

@keyboardDrummer : Thanks for digging into the flaky CI issues. I had also noticed these small tests failing in CI with a timeout and had no idea what was going on.

Fix a bug that could cause a concurrency related exception in QuantifierInstantiationInfo, which was introduced by #862.

To improve my understanding, could you say a bit more about the bug introduced by my aforementioned PR?

[keyboardDrummer]

To improve my understanding, could you say a bit more about the bug introduced by my aforementioned PR?

The fix is in this commit: c79011b
While running tests, I saw a concurrent modification exception during a call to HashSet.Add done from FindInstantiationHints. Looking at the git history, FindInstantiationHints was originally designed to be able to be called concurrently, but since the introduction of the HashSet it no longer supported this. I replaced the use of HashSet with a ConcurrentBag so it can handle concurrent Add calls.