Unfortunately this is caused by a nontermination bug in the maude backend
of krun. The program does not actually loop forever, it is merely that the
compiled definition in maude is loaded and has errors, and the bug causes
krun to not crash with an error message. I have a pull request now that
should address this issue, which will be merged into the unified builtins
branch soon. In the meantime, I suggest you do the following:

1. Reload the change that you made before with the removed code from
FlattenTerms and the Variable.setSort call
2. Try compiling the example again, then run, from the main k directory:

```
$ lib/maude/binaries/maude.linux
Maude > load
tests/regression/label-and-context/label-and-context-kompiled/main.maude

This should show you the errors that you will need to resolve.


On Tue, May 20, 2014 at 10:36 AM, Liyi Li <notifications@github.com> wrote:

> In
> src/javasources/KTool/src/org/kframework/compile/transformers/ResolveSyntaxPredicates.java:
>
> > @@ -38,7 +44,8 @@ public ASTNode visit(Sentence node, Void _)  {
> >          for (Variable var : vars) {
> >  //            if (!var.isUserTyped()) continue;
> >              if (var.isSyntactic()) continue;
> > -            if (MetaK.isKSort(var.getSort())) continue;
> > +            if ((var.getExpectedSort()==null && MetaK.isKSort(var.getSort()))
>
> Because there solution is wrong. I cannot even run some program. The
> program will loop forever.
> for example:
> If I have this definition:
> // Copyright (c) 2013-2014 K Team. All Rights Reserved.
> /*
> Expected:
> 'ListWrap(1,,1,,1)
> */
> module LABEL-AND-CONTEXT
> configuration $PGM:K
>
> syntax KLabel ::= "'ListWrap" | "'A"
> syntax KResult ::= Int
> context 'ListWrap(*,,HOLE,,*)
>
> rule 'A(_) => 1
> endmodule
>
> and run this program:
> 'ListWrap('A(.KList),,'A(.KList),,'A(.KList))
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/466/files#r12850577>
> .
>