In the current version method TPABase::getSafetyExplanation does not work correctly if the safety has been proven using (left or right) transition invariants collected in the Houdini check.
The problem is that the method in the current version still relies on the information stored in explanation.power, but this information is not (and cannot) be filled in the case mentioned above.
The proposed solution is to store directly the transition invariant in the explanation, instead of implicitly relying on the assumption that the invariant is one of the abstract transitions.
In the current version method TPABase::getSafetyExplanation does not work correctly if the safety has been proven using (left or right) transition invariants collected in the Houdini check.
The problem is that the method in the current version still relies on the information stored in explanation.power, but this information is not (and cannot) be filled in the case mentioned above.
The proposed solution is to store directly the transition invariant in the explanation, instead of implicitly relying on the assumption that the invariant is one of the abstract transitions.