Unable to verify lemma with interactive GUI

[Andy Hammer]

Hello all,

I'm creating a model that includes a high-level abstraction of secret sharing/message splicing. Unfortunately, I've seen to run into a bug that I am struggling to resolve. As part of a MWE, I have used a debugging lemma to identify this trace using the interactive GUI.

In the trace, it identifies there is a trace that includes the action fact "Debug('Complete')". In a separate lemma, I attempt to prove that at some time stamp, this action fact occurs. However, trying to automatically prove this results in the process being killed and attempting to prove it myself with the interactive prover results in finding a trace up to the rule, (with all premises satisfied) but never progressing through it.

There seems to be a loop when working with the interactive prover that I am unable to navigate out of. I attempted using some of the different flags and changing the chain length and using auto-sources to mitigate this issue, but seem to be unable.

Is there any advice anyone can provide?

Thank you in advance! Andy.