Errors when loading *-analyzed.spthy files from ./case-studies-regression

[Nynko]

Hello,

I have stumbled into errors on several files while doing some tests.
This issue will be updated with further details

They are all analyzed files but I haven't check the errors on all of them.
Here is a list of all the files that did crashed during test: FilesErrors.txt
(There are some duplicates in different folders)
[EDIT]: As diff files would necessarily crash without the diff flag, there are only few files that crash:

./case-studies-regression/related_work/YubiSecure_KS_STM12/Yubikey_analyzed.spthy
./case-studies-regression/regression/trace/issue193_analyzed.spthy

One example is on ./case-studies-regression/related_work/YubiSecure_KS_STM12/Yubikey_analyzed.spthy which throw this error:

tamarin-prover: "./case-studies-regression/related_work/YubiSecure_KS_STM12/Yubikey_analyzed.spthy" (line 199, column 9):
unexpected "n"
expecting "case", "qed", "SOLVED", "by", "sorry", "simplify", "solve", "contradiction" or "induction"
CallStack (from HasCallStack):
  error, called at src/Theory/Text/Parser/Token.hs:208:21 in tamarin-prover-theory-1.7.1-EvrwkKoaLjS4nIQn8mTw3V:Theory.Text.Parser.Token

[jdreier]

I had a quick look at case-studies-regression/related_work/YubiSecure_KS_STM12/Yubikey_analyzed.spthy, at various places there are spurious empty cases, which cause the parser to fail:

    solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 )
     case 
     by sorry /* unannotated */
   next
     case BuyANewYubikey
     by contradiction /* cyclic */

Funnily enough, these empty case seem to exist since the initial commit in 2012.

[rkunnema]

Funnily enough, these empty case seem to exist since the initial commit in 2012.

If by empty case you mean the by sorry, that was on purpose. At the time, we did not have oracles, and that was a way to guide the proof. The "by sorry" is resolved when calling with --prove. We need to support this feature anyway, because the interactive mode may save incomplete proofs.

Weirdly, I don't get this error with the current develop when calling tamarin-prover examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy.

[jdreier]

This does not concern the example file, which works well. It concerns the output of Tamarin after running this example file, which is stored in case-studies-regression, not in examples.

By empty case I mean the case keyword followed by nothing, although there should be a case name. And in the verified file, there should not be a by sorry either.

[jdreier]

But I have the impression that this is essentially a display problem, the real first subcase for this goal is the following one, called BuyANewYubikey, which is correctly solved.