@@ -10,6 +10,6 @@ Hereby, `<filename>` has to be replaced with the name of the file that shall be
Depending on `<filename>`, the heuristic should be set to `I` or `S` to optimize verification times. For `daa_pnc_credential_installation.spthy` use `--heuristic=S`.
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 commandline `--heuristic=<I|S>` argument in Tamarin version 1.6.0.
Some lemmas use an oracle heuristic (via `[heuristic=o]` at the lemma definition), which overwrites the commandline `--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).
\ No newline at end of file
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).
