transparent function == verified multiple times?

[hmijail]

What change in documentation do you suggest?

If using --filter-symbol outer, where outer() calls the transparent function inner(), is inner verified inside of outer so that it contributes to what the solver "knows" inside of outer?

Experimentation shows that even with filter-symbol outer, verification failure in inner is reported, so looks like the the answer would be positive.

So, does this mean that without filter-symbol the function inner would be verified twice? (or as many times as it is called inside other functions/methods)

[keyboardDrummer]

If using --filter-symbol outer, where outer() calls the transparent function inner(), is inner verified inside of outer so that it contributes to what the solver "knows" inside of outer?

It might help you to think in terms of assertions when considering what is verified or not. Every explicit or implicit assertion in the Dafny program is only verified at most once. The body of a function may be used in the verification of different assertions, but that does not mean the function is verified multiple times.

predicate P(x: int) {
  true && Q()
}

predicate Q() {
  false
}

method Foo() {
  assert P(0); // This assertion failure references P and Q
  assert P(1); // This assertion failure also references P and Q, 
  // but we do not say that P or Q are verified more than once.
}

When I say a function is verified, then I mean that any explicit or implicit assertions that occur inside that function body are verified, which does not relate to any calls to that function. Here's an example of a function that verifies and one that does not:

function P(x: int): int {
  x / 3; // implicit assertion "3 != 0", verifies successfully
}

function Q(x: int): int {
  x / 0; // implicit assertion "0 != 0", fails to verify
}