Diff vs Variants

[sbursuc]

Hi,

I want to specify manually variants for an observational equivalence query, and I get this error:

"
Error in mergeLeftRightRulesDiff. Please report bug.
CallStack (from HasCallStack):
error, called at src/OpenTheory.hs:517:72 in tamarin-prover-theory-1.8.0-2wJAxLkm1ct5mTfd9OWFEB:OpenTheory
"
I copy below a simple input file illustrating the problem. The variants are exactly the same on left and right, so I don't know where the missmatch happens. While the issue is fixed, please let me know if and how I could obtain the intended behaviour on a current version of Tamarin.

Thanks.
Sergiu

theory VARIANTS_DIFF
begin

builtins: diffie-hellman

rule Diff:[]-->[ !T(diff('a','b')) ]
rule Exp: [ In(y), !T(x) ] --> [ Out(x^y) ]

left rule Exp: [ In(y), !T(x) ] --> [ Out(x^y) ]
variants rule (modulo AC) Exp_Var:
[ In(y), !T(x) ] --> [ Out(x^y) ]

right rule Exp:[ In(y), !T(x) ] --> [ Out(x^y) ]
variants rule (modulo AC) Exp_Var:
[ In(y), !T(x) ] --> [ Out(x^y) ]

end

[rsasse]

In case you just do not give a left and right instantiation, Tamarin will produce them for you (see in the GUI), so whatever is created there would be the intended behavior, I guess. Have you checked whether the automatically generated variants for the sides, if you only give the rule without variants, are exactly as you gave them in this example?

I expect in your actual model you do want them to be different, but I do not know what the issue is here and how to help you with that. Maybe @jdreier has an idea?

[jdreier]

I can open the file in interactive mode without any problem (I just get the expected warning), but this fails in command line mode with the error message mentioned. I will dig into this, but in the meantime using interactive mode seems to be a possible workaround.