A potential bug in how Silicon handles loop invariant

[funemy]

Hi!

The example below fails to verify in Silicon, but verifies in Carbon (using the most recent release of the viper vscode plugin).

The places that seem relevant are commented with // FIXME:.
If I switch the order of the last two invariants in the inner loop, then the code gets verified in Silicon as well.

Seems like a potential bug in handling loop invariant?

domain Matrix {
  function select(m: Matrix, i: Int, j: Int) : Int
  function store(m:Matrix, i: Int, j:Int, value: Int) : Matrix
  function size(m:Matrix) : Int // only one size function needed for a square matrix (number of rows and number of columns)
  axiom select_store_same {
    forall m: Matrix, i: Int, j:Int, v:Int :: {select(store(m,i,j,v),i,j)} inRange(m,i,j) ==> select(store(m,i,j,v),i,j) == v
  }
  axiom store_preserve_size {
    forall m: Matrix, i: Int, j: Int, v: Int :: {store(m,i,j,v)} inRange(m,i,j) ==> size(store(m,i,j,v)) == size(m)
  }
  axiom select_store_diff {
    forall m: Matrix, i1: Int, j1:Int, i2: Int, j2:Int, v : Int :: {select(store(m,i1,j1,v),i2,j2)} {select(m,i2,j2),store(m,i1,j1,v)}
      inRange(m,i1,j1) && inRange(m,i2,j2) && (i1 != i2 || j1 != j2) ==> select(store(m,i1,j1,v),i2,j2) == select(m,i2,j2)
  }
}

define inRange(m,i,j) 0 <= i && 0 <= j && i < size(m) && j < size(m)

method add(m1: Matrix, m2: Matrix) returns (m3: Matrix)
  requires size(m1) == size(m2)
  ensures forall x:Int, y:Int :: {select(m3,x,y)} inRange(m1,x,y) ==> select(m3,x,y) == select(m1,x,y) + select(m2,x,y)
{
  assume size(m3) == size(m1) // "initialise" m3 to *some* matrix of the right size
  var i : Int := 0
  var j : Int
  while(i < size(m1))
    invariant i >= 0
    invariant size(m3) == size(m1)
    // FIXME: fails to be reestablished (with Silicon)
    invariant forall x: Int, y: Int :: {select(m3,x,y)} 0 <= x < i && 0 <= y < size(m1) ==> select(m3,x,y) == select(m1,x,y) + select(m2,x,y)
  {
    j := 0
    while(j < size(m1))
        invariant i >= 0
        invariant j >= 0
        invariant size(m3) == size(m1)
        // FIXME: if we switch the order of the two invariants below, the program verifies in both Silicon and Carbon
        invariant forall y: Int :: {select(m3,i,y)} 0 <= y < j ==> select(m3,i,y) == select(m1,i,y) + select(m2, i, y)
        invariant forall x: Int, y: Int :: {select(m3,x,y)} 0 <= x < i && 0 <= y < size(m3) ==> select(m3,x,y) == select(m1,x,y) + select(m2, x, y)
    {
      m3 := store(m3,i,j,(select(m1,i,j) + select(m2,i,j)))
      // assert select(m3,i,j) == select(m1,i,j) + select(m2,i,j)
      j := j + 1
    }
    i := i + 1
  }
}

[marcoeilers]

I looked into this and it is truly bizarre. As far as I can see, the SMTLIB emitted by Silicon is correct. It cannot be a Z3 issue though, because CVC5 agrees.
Attached is a derived file where adding an assume statement to a Viper program that verifies makes it no longer verify (in Silicon), which may or may not be related but is equally bizarre to me.

test.vpr.txt

[funemy]

I took a closer look at the differences between the log files before and after switching the order of the two inner loop invariants.

Indeed, the SMT constraints emitted by Silicon all seem correct and mostly identical (with the major difference being the order of re-establishing the inner loop invariants).

I think the the issue is indeed due to Z3 (and maybe CVC5 as well..?).
I noticed that if I rewrote the first inner loop invariant from:

 invariant forall y: Int :: {select(m3,i,y)} 0 <= y < j ==> select(m3,i,y) == select(m1,i,y) + select(m2, i, y)

to

 invariant forall x: Int, y: Int :: {select(m3,x,y)} x == i && 0 <= y < j ==> select(m3,x,y) == select(m1,x,y) + select(m2,x,y)

Then the example gets verified by Silicon.

But it's still confusing to me why switching the order of of the two invariants in the original case gets the code verified.