title: Invariant fails but assert before loop verifies
body: <p>In the following program, the last invariant of the loop fails to verify. But if I put it as an assert before the while loop, the condition verifies. If I add that the field <code>ia</code> does not change, it also verifies. Why is this needed? Shouldn't this be implied by the read permissions? I can imagine that <code>old</code> interacts in a weird way with the loop pre-state/havocking of the state, but that doesn't explain to me why it fails. Could it be a bug?</p>
  <pre><code>domain VCTArray[CT] {
    function loc(a: VCTArray[CT], i: Int): CT
    
    function alen(a: VCTArray[CT]): Int
  }
  
  //  a field 
  field ia: VCTArray[Ref]
  
  //  a field 
  field item: Int
  
  method negatefirst(diz: Ref)
  requires diz != null
  requires acc(diz.ia, 1/2)
  requires alen(diz.ia) &gt; 0 ==&gt; acc(loc(diz.ia, 0).item, write)
  {
    // Verifies just fine
    assert alen(diz.ia) &gt; 0 ==&gt; (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item))
    while (false)
      invariant acc(diz.ia, 1/4) 
      // invariant diz.ia == old(diz.ia) // Adding this invariant allows the program to verify
      invariant alen(diz.ia) &gt; 0 ==&gt; acc(loc(diz.ia, 0).item, write)
      // Error: insufficient permission to acces loc(diz.ia, 0).item
      invariant alen(diz.ia) &gt; 0 ==&gt; (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item)) 
    { 
      
    }
  }
  </code></pre>
  <p>My silicon version:</p>
  <pre><code>$ ./silicon.sh --help
  Silicon 1.1-SNAPSHOT (d45da1d7+)
  </code></pre>