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 PR fixes two issues:
In a quantifier with trigger
f(e)
, it could happen that if the quantifier body containedold(f(e))
, that Silicon accidentally emitted a trigger essentially equivalent toold(f(e))
instead of the intended trigger (that's the problem behind issue #509). The reason is that when remembering what terms expressions evaluate to, Silicon did not take into acountold
, so when evaluatingold(f(e))
to some termt
during the evaluation of the quantifier body, it would incorrectly remember thatf(e)
evaluates tot
, and thus translate a triggerf(e)
accordingly. Now, Silicon correctly remembers thatt
is the value ofold(f(e))
.Second, Silicon used to discard
old
on the outside of trigger expressions. So if the user supplied a triggerold(e)
, Silicon would treat this as if they'd just writtene
. Now it no longer does this.