shazqadeer
commented
2 years ago @keyboardDrummer : The comment referenced in the issue description does not provide enough detail. Could you please expand the issue summary with the following information:
- What doesn't work? In other words, what is the manifestation of the problem?
- Why do you even expect that you ought to be able to reuse checkers?
Tests using snapshots fail unless a new ExecutionEngine is created per snapshot. This is surprising since an ExecutionEngine is meant to be re-usable as long as the passed CLI options are the same. The issue seems to be caused by the re-use of checkers between snapshots, which should but doesn't work. Checkers are designed to be re-usable, they can be targeted to different programs, as long as the same CLI options are used.
https://github.com/boogie-org/boogie/blob/master/Source/ExecutionEngine/ExecutionEngine.cs#L101