Carbon does not properly stop Boogie (and the Z3 processes created by Boogie)

[viper-admin]

Created by @aterga on 2018-01-19 16:50

Running Viper frequently, e.g., in the IDE, requires the verification jobs to be stoppable in constant (or near constant) time. Silver's trait Verifier provides a stop method which is used by whoever wants to terminate a running verification session.

However, Carbon's implementation of stop does not terminate the child Boogie process. It just blocks until it finishes. See BoogieInterface.stopBoogie().

[fabiopakk]

I've fixed this issue and tested on a Mac successfully. However, as I've commented on the above mentioned function, all platforms should be tested to ensure this solution is portable. This issue should be reopened otherwise.