Proof Log Files

In the course of its execution Snark typically outputs a lot of information as well as a proof when it finds one. All this output can be overwhelming to the user, yet invaluable in understanding why the proofs succeeded or failed. To deal with all this output Specware redirects all the Snark output to log files. In our example above, which executed a proof in the file pruf.sw, Specware will create a subdirectory called Snark at the same level as pruf.sw. In that directory a log file called pruf.log will be created that contains all the Snark output.