Exception when Boogie exits

[shazqadeer]

Recently, I have noticed that Boogie routinely crashes towards the end of processing when I run Boogie under a debugger. The typical problem is that task has exited but some state pertinent to the task is being examined. The phenomenon appears to be new. I was wondering if any of the folks who have done commits to Boogie recently may have some insights into why this is happening. I will post more information about the location of the crash next time I encounter it.

cc: @keyboardDrummer , @atomb

[keyboardDrummer]

Can you say more about the crash? Is there a particular exception?

Maybe this commit improves the problem: fcf0dde

[shazqadeer]

I ran "Test/bitvectors/bv5.bpl -proverOpt:BATCH_MODE=true" on the master version of Boogie in JetBrains Rider and got an exception at this line.

System.InvalidOperationException: Cannot process request because the process (45793) has exited.
   at System.Diagnostics.Process.ThrowIfExited(Boolean refresh)
   at System.Diagnostics.Process.EnsureState(State state)
   at System.Diagnostics.Process.get_UserProcessorTime()
   at Microsoft.Boogie.SMTLib.SMTLibProcess.Close() in /Users/shaz/Source/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 290

[atomb]

That's very strange. The line at the root of that stack trace is inside a try block with catch (Exception e), so the fact that an InvalidOperationException is escaping is surprising.

[atomb]

That's very strange. The line at the root of that stack trace is inside a try block with catch (Exception e), so the fact that an InvalidOperationException is escaping is surprising.

That is, the line that invokes Process.get_UserProcessorTime().

[shazqadeer]

I was being inaccurate when I said in my original issue that "Boogie crashes". I really meant that I was seeing these exceptions when a process was being accessed after it had already exited. The exception seemed harmful and unintended. Is the code logic such that an exception like this is normal behavior?

[keyboardDrummer]

I was being inaccurate when I said in my original issue that "Boogie crashes". I really meant that I was seeing these exceptions when a process was being accessed after it had already exited. The exception seemed harmful and unintended. Is the code logic such that an exception like this is normal behavior?

I'm guessing such an exception is a bug in the dispose logic, probably harmless for users, but could be harmful during testing and it is better to resolve.