As there can be multiple units per file, there can be multiple proof units in single file. For example, in file pruuf.sw we could include more than one proof unit, as follows:
p1 = prove prop1 using ax1, ax2
p1a = prove prop1 using ax3
p2 = prove prop2 |
In this case proc pruuf will invoke Snark three separate times, writing three different log files. In this case an additional subdirectory will be created under Snark, called pruuf. The three log files will then be: Snark/pruuf/p1.log, Snark/pruuf/p1a.log, and Snark/pruuf/p2.log.