Two methods (with sequences and quantified permissions) are verified on their own, but Carbon does not terminate when verifying both

[tdardinier]

Carbon does not terminate on the following Viper program (corresponding to quantifiedpermissions/sequences/seq_pure.vpr in the Silver test suite). However, it terminates in 9s if I comment out test01, and in 3s if I comment out test04.

field f: Int

method test01(S:Seq[Ref], a:Int)
  requires 0 <= a && a < |S|
  requires forall j1: Int, j2: Int :: {j1 in [0..|S|), j2 in [0..|S|) } j1 in [0..|S|) && j2 in [0..|S|) && j1 != j2 ==> S[j1] != S[j2]
  requires forall j:Int :: j in [0..|S|) ==> acc(S[j].f, write)
  requires forall j:Int :: j in [0..|S|) ==> S[j].f > 0
  ensures forall j:Int :: j in [0..|S|) ==> acc(S[j].f, write)
  ensures forall j:Int :: j in [0..|S|) ==> S[j].f > 0
{
  S[a].f := 2
}

method test04(S:Seq[Ref], a:Int)
  requires 0 <= a && a < |S|
  requires forall j1: Int, j2: Int :: {S[j1], S[j2]} j1 in [0..|S|) && j2 in [0..|S|) && j1 != j2 ==> S[j1] != S[j2]
  requires forall j:Int :: j in [0..|S|) ==> acc(S[j].f, write)
  requires forall j:Int :: j in [0..|S|-1) ==> S[j].f <= S[j+1].f
  ensures forall j:Int :: j in [0..|S|) ==> acc(S[j].f, write)
  //:: ExpectedOutput(postcondition.violated:assertion.false)
  ensures forall j:Int :: j in [0..|S|-1) ==> S[j].f <= S[j+1].f
{
  S[a].f := 5
  assert forall j:Int :: j in [0..|S|-1) ==> j in [0..|S|)
}