the PTL steps in proofs do not work, this can be caused by either:
- there is a problem in the build of the LS4 prover
- there is a problem in the build of the ptltotrp utility
- there is a bug in the PM
In case the tool stopped working after a change in the system (a version upgrade, etc.) it is recommended that the PM will be re-installed in order to rebuild the ptl_to_trp utiility. In case you want to build it yourself, please download it from:ptl_to_trp
run buildAll.sh, rename the resulted translate object to ptl_to_trp and use it to replace the previous object.