Autoprove does not produce the same result as keep solving the first goal

[Yan Peng]

Hi all,

I'm new to Tamarin and I've encountered some performance issues. I noticed that in the GUI, if I keep pressing the first goal (I've defined an oracle for guiding the proof), I end up finding a trace quite fast. However, if I use autoprove, the solver will run for a very long time. 

I found two issues that have similar problems:

https://github.com/tamarin-prover/tamarin-prover/issues/343

https://github.com/tamarin-prover/tamarin-prover/issues/118

In issue 118, it was mentioned that the reason for this problem is that Tamarin uses iterative deepening.

I'm wondering if there is a way of disabling iterative deepening for a lemma? Even better, is there a way of making autoprove do exactly what is achieved with pressing the first goal? I tried the solution of adding --stop-on-trace=BFS as is mentioned in issue 118, and it didn't work for me.

Cheers,

Yan