Bug in RewritePolymorphicSelect

[FedericoAureliano]

Nested polymorphic selects are not being rewritten correctly in combination with function calls.

For example, the following code gives a spurious type error.

module main {
  type r1 = record {x: integer};
  type r2 = record {y: r1};
  function z(): r2;
  init {
    assume(z().y.x == 0);
  }
}

I'm pretty sure the issue here. Even if it is not there, for some reason we are deciding that we shouldn't rewrite x to _rec_x and that is causing the problem.

[lichye]

Hello Federico,
rewriting x to _rec_x is how the record rewriter is supposed to do. But is rewriting x to _rec_x gives x a incorrec type? And rec does not mean " x is a record" but mean "x is owned by a record". I will look into that and fix up this bug.