When using rodin to prove proof obligations, sometimes the prove tree will lost after rebuild.
The workspace is attached and you can reproduce the problem very easily.
There are one project in the workspace: MathematicalObjects.
There are 3 machines and 6 Theories in the project.
Some of the proof obligations are proved with the help of theories.
To reproduce the problem:
1. Initially all the proof obligations of the 3 machines are successfully proved.
2. Then I clean all the projects in the workspace. After rebuild, I deploy the 6 Theories.
3. A lot of previously proved proof obligations are now marked as unproved.
This bug was initially reported by Shawn Zhang <firstname.lastname@example.org> on the user mailing list.
Unfortunately, an archive of the workspace is too large to be attached to this bug report. It is available from me.
Log in to post a comment.