This warning occurred with the following code:

```
predicate ExistsSingleInstance(s : string32, delim : string32)
{
exists pos : nat ::
(pos <= |s| - |delim| && forall x : nat :: x < |delim| ==> s[pos + x] == delim[x]) &&
forall pos' : nat :: (pos' <= |s| - |delim| && forall y : nat :: y < |delim| ==> s[pos' + y] == delim[y]) ==> pos == pos'
}
```

The verifier uses quantifications by finding good ways to instantiate them.
More precisely, it uses `forall`

quantifiers by instantiating them and it proves `exists`

quantifiers by finding witnesses for them.
The warning you’re getting says that nothing stands out to the verifier as a good way to figure out good instantiations.

In the case of `pos`

, this stems from the fact that a good instantiation would be some `pos`

for which the verifier already knows either `pos <= …`

or `forall x :: …`

, the former of which is not specific enough and the latter is too complicated for it to consider.

The “no trigger” warning is fixed by this refactoring:

```
predicate SingleInstance(s: string, delim: string, pos: nat)
{
pos <= |s| - |delim| &&
forall x : nat :: x < |delim| ==> s[pos + x] == delim[x]
}
predicate ExistsSingleInstance'(s: string, delim: string)
{
exists pos : nat ::
SingleInstance(s, delim, pos) &&
forall pos' : nat :: SingleInstance(s, delim, pos') ==> pos == pos'
}
```

One more remark: The “no trigger” warning should be taken seriously, because it’s usually a sign that there will be problems with using the formula and/or problems with verification performance.