Fix a small problem with triggers on spec_fn closures and deprecate triggers on spec_fn closures #1038
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is related to #331 and #1033 . It fixes the minor problem from #1033 . However, looking at this more closely, I think manual triggers on spec_fn closures cannot be supported in general because the AIR-generated axiom for spec_fn closures quantifies over "holes" that are not visible to source-level quantifiers. The built-in trigger generated by AIR works fine with these holes, but manual triggers do not because they have no way to name the holes. The examples in #331 happened to work because there were 0 holes in those examples, but for more complex cases (like the one in #1033 ), the manual triggers just lead to a Z3 warning "WARNING ... pattern does not contain all quantified variables" and are subsequently dropped by Z3. Therefore, I believe that this feature (manual triggers on spec_fn closures) should be deprecated. The discussion in #331 provides a way to work around the absence of this feature.