Troubleshooting

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.

Last edited Nov 18, 2014 at 1:16 PM by libal, version 6