@@ -13,3 +13,5 @@ For both `daa_pnc_charge_authorisation_*.spthy` models use `--heuristic=I`.
Some lemmas use an oracle heuristic (via `[heuristic=o]` at the lemma definition), which overwrites the command line `--heuristic=<I|S>` argument in Tamarin version 1.6.0.
As the python oracle is used during verification, it is important that it is located in the same folder as the command is run (and that the oracle file is executable).
By default, Tamarin prints its verification steps to the console. Note that the most important output is the **summary of summaries** at the end of execution, which should indicate that all lemmas were **verified**.
