Explication bug

[casperbp]

Seems there's a bug in explicate-premise. The following definition crashes during explication:

module ds/l09

signature

    sorts Expr Cmd Val Scope FrameId Label Occurrence H

    arrows
        Cmd -cmd-> Val
        Expr --> Val

    constructors
        Decl : String * Expr * Cmd -> Cmd

    native operators
        getCmdScopes : Cmd -> List(Scope)

    sorts initDefault__Arrow set__Arrow
    constructors
    initDefault : Scope * Map(Label, Map(Scope, FrameId)) -> initDefault__Arrow
    set : Occurrence * Val -> set__Arrow     
        getOcc : String -> Occurrence
        P                : Label
  arrows
    initDefault__Arrow -initDefault-> FrameId
    set__Arrow -set-> H

    variables
        h : H
        f : FrameId
        v : Val

rules

    // DynSem's explicate-premise strategy fails on this term:
    f |- c@Decl(x, v, c') -cmd-> v'
    where
        getCmdScopes(c) => [s1, s2];
        initDefault(s2, {P() |--> {s1 |--> f}}) -initDefault-> f' :: h;
        f', h |- set(getOcc(x), v) -set-> h';
        f' |- c' :: h' -cmd-> v'.

//  // DynSem's explicate-premise strategy succeeds on this term:
//  f |- c@Decl(x, v, c') :: h0 -cmd-> v' :: h3
//  where
//      getCmdScopes(c) => [s1, s2];
//      initDefault(s2, {P() |--> {s1 |--> f}}) :: h0 -initDefault-> f' :: h1;
//      f', h1 |- set(getOcc(x), v) -set-> h2;
//      f' |- c' :: h2 -cmd-> v' :: h3.

Error:

org.metaborg.core.transform.TransformException: Invoking Stratego strategy module-to-core-editor failed at term
    Formula(
  Relation(
    Reads([])
  , Source(VarRef("_lifted_54"), [])
  , NamedDynamicEmitted([], "initDefault")
  , Target(
      VarRef("_lifted_55")
    , [LabelComp(SimpleSort("H"), VarRef("h"))]
    )
  )
)
Stratego trace:
    module_to_core_editor_0_0
    module_to_core_editor_0_0
    module_to_core_0_2
    in_project_path_1_1
    dr_scope_1_1
    explicate_module_0_0
    m_in_extracted_components_1_0
    explicate_rules_0_0
    alltd_1_0
    explicate_rule_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premises_0_0
    explicate_premise_0_0
    report_with_failure_0_1
    report_failure_0_2
    SRTS_EXT_fatal_err_0_2

    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:140) ~[org.metaborg.spoofax.core_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:65) ~[org.metaborg.spoofax.core_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:1) ~[org.metaborg.spoofax.core_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.core.transform.TransformService.transform(TransformService.java:55) ~[org.metaborg.core_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.core.transform.TransformService.transform(TransformService.java:42) ~[org.metaborg.core_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.transform(TransformJob.java:141) [org.metaborg.spoofax.eclipse_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.transformAll(TransformJob.java:108) [org.metaborg.spoofax.eclipse_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.run(TransformJob.java:70) [org.metaborg.spoofax.eclipse_2.1.0.20160809-125800-feature_scopes-and-frames.jar:na]
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55) [org.eclipse.core.jobs_3.8.0.v20160509-0411.jar:na]
[...]

However, if one uncomments the second rule in the example program, explication succeeds.