Manually defining uninterpreted functions can lead to core dump

[cascremers]

Here's a nice core dump:

The reason does not seem to be the 'let'. Instead, the dump is caused by me using H1/H2 as below. This causes Maude to bork (in some examples silently, in this one with an error) but Tamarin core dumps.

theory NAXOS_eCK
begin

builtin: diffie-hellman

functions: H1/1
functions: H2/1

section{* NAXOS *}

rule generate_ltk:
   let pkA = 'g'^~lkA
   in
   [ Fr(~lkA) ] -->
   [ !Ltk( $A, ~lkA ), !Pk( $A, pkA ), Out( pkA ) ]


rule Resp_1:
  let pkI    = ('g'^~lkI)
      exR    = H1(< ~ekR, ~lkR >)
      hkr    = 'g'^'4'
      seskey = H2(< pkI^exR, X^~lkR, X^'6', $I, $R >)
  in
   [ In( X ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, pkI) ]
   --[ SidR_1( ~ekR, $I, $R, X, hkr, seskey) ]->
   [ Out( hkr ),
     !Ephk(~ekR),
     !Sessk( ~ekR, seskey) ]

end

[cascremers]

Added note: replacing H1 and H2 by 'h' removes the problem.

[beschmi]

Our parser for maude output does not expect numbers in the function symbols. This will be fixed together with
issue #6.

No idea why GHC crashes with:

tamarin-prover: internal error: scavenge_stack: weird activation record found on stack: 12352
(GHC version 7.4.1 for i386_apple_darwin)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Abort trap: 6