Conflicting variables in data gives wrong results in certain cases about mcrl2 HOT 3 CLOSED

A simpler example showing the problem is:

map e:Bool;
eqn e = exists t':Nat. t' in { x: Nat | exists t':Nat.(t'==3+x && x==4) };

The expression e rewrites to false, but should rewrite to true. Rewriting to false is due to substituting the outer t' for x, which is subsequently captured by the inner exists, changing the meaning of the formula. The reason for the problem is an inadequate test in the data enumerator inside the rewriter. This test will soon be adapted, resolving the problem.

from mcrl2.

The problem is not related to #1629 and #1644, although they all fall in the realm of the troubling world of bound variables.

from mcrl2.

Problem is resolve in commit ddb7fbf.

from mcrl2.