Okay, this is a failure in test design. If the name of the key of this map
is unspecified, then we shouldn't specify it in the test output. is there a
way to specify a k pattern that the output of this program should match?
On Mar 7, 2014 12:29 PM, "Yilong Li" <notifications@github.com> wrote:

> In tests/regression/java-rewrite-engine/smt_model/program.test.out:
>
> > @@ -1,3 +1,3 @@
> >  <k>
> > -    _0!0:Int |-> 1
>
> _0!0 is a generated fresh variable. The name often get changed as we
> change the implementation. In this case, it got changed because I fixed a
> bug related to detecting unbound variables on the RHS of a rule.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/270/files#r10398533>
> .
>