Assign value of an array using another array

[wmanshu]

Is it possible to support such assignment:

struct AData {
  var amount: [Int]

  public init(_amount: [Int])
  mutates (amount)
  {
    self.amount = _amount
  }
}

Also, this now gives anIllegal modification of variable not declared in 'mutates(...)' error

[wmanshu]

I am not sure if Flint support this. Because it can compile when --skip-verifier. But still shows error when not skip verifier

[mrRachar]

This is actually a known verifier issue, and is related to #436, and can be currently fixed by provided many type-level modifies identifiers. There is work being done on this right now in matteobilardi/flint which should hit later today.

[mrRachar]

Unfortunately it appears that this issue goes a little deeper, there seem to be some mutated array variables that aren't handled correctly by the verifier