Example: This code

class {:autocontracts} A {
ghost predicate Valid() {
true
}

constructor() {
// no-op
}
}

class {:autocontracts} B {
var things: set<A>

ghost predicate Valid()
{
forall thing | thing in things :: thing.Valid()
}

constructor() {
things := {};
}
}



produces this output:

ERROR_InsufficientReads.dfy(17,48): Error: insufficient reads clause to invoke function

Dafny program verifier finished with 3 verified, 1 error



This error message indicates that a nested call of a function needs a bigger reads set than its enclosing function provides.

Another situation provoking this error is this:

class A {
var x: int
x == 2
}
}
type Ap  = x : A | x.IsSpecial() witness *


In this case the error message is a bit misleading. The real problem is that the predicate in the subset declaration (that is, x.IsSpecial()) is not allowed to depend on the heap, as IsSpecial does. If such a dependency were allowed, then changing some values in the heap could possibly change the predicate such that a value which was allowed in the subset type now suddenly is not. This situation would be a disaster for both soundness and ease of reasoning.

Another variation on the above is this example:

trait A { var x: int }
type AZero = a: A | a.x == 0 witness *


where again the predicate depends on a heap variable x, which Dafny does not permit.

And a final example:

datatype Foo = Foo | Foofoo

class Bar {
var foo: set<Foo>;
function method getFoo(): set<Foo> { this.foo }
}


which produces Error: insufficient reads clause to read field. In this case the function getFoo does indeed have an insufficient reads clause, as it does not have one, yet it reads a field of this. You can insert either reads this or reads thisfoo before the left brace.

The code in the original question is fixed like this:

class A {
true
}

constructor() {
// no-op
}
}

class B {
var things: set<A>

predicate Valid()
`