adding reads {} in a recursive function call causes the verification to fail

Question

function f(bs:seq<bool>, hi:nat) : nat
  reads {}
{
  if hi==0 then 0 else f(bs, hi-1)
}

method Main() {
  var arr := [false, false, false];
  assert f(arr, 2) == 0;
}

The assertion assert f(arr, 2) == 0; fails to verify. However, if I remove reads {}, it passes.

In my actual code, I must use reads. I want to know why even just adding reads {} still affects the verification. What statement should I add to prompt Dafny?

Answer 1

A Reads set is only required for functions or method which operate on mutable data. Arrays and classes are mutable. Sets, maps, seqs, etc.. are all immutable and don't require reads.