False negative for postconditions with `this` or `#n` in their expression

Commit d70dd7436fa9a6706db40be85978ac4dd04d2a18 introduces a false negative, in its use of CFAbstractStore.insertValuePermitNondeterministic(). Consider this test case:

import java.util.Optional;

class PureGetterTest2 {

  Optional<String> otherOptional() {
    if (Math.random() < 0.5) {
      return Optional.ofNullable(null);
    } else {
      return Optional.of("hello world");
    }
  }

  void foo() {
    if (otherOptional().isPresent()) {
      // BUG: no "method.invocation" error is issued here.
      otherOptional().get();
    }
  }
}

In a postcondition like @EnsuresPresent("field.method()"), it is correct to permit method() in the expression even if it is not @Deterministic. However, in a postcondition like @EnsuresPresent("#1.method()"), it should not be permitted to substitute in an argument that is not @Deterministic.