Is it ok to remove this code?

Yes, unless the test suite shows us otherwise.
When you do remove it, please also remove the unused variable pr on L1772.

I think it would be good to do the analogous change also for multisets. You could do that in this same PR, in a separate PR, or, if nothing else, file an Issue that reminds us that this would be a good change to make in the future.

I'll do this in this PR if it's not too hard

I think it would be good to do the analogous change also for multisets

Done ! That wasn't too hard. The only difference was that the trigger expressions were of the form (A + B)[x] and so this is what I split into two new triggers A[x] and B[x] (if the bound variables are the same of course!)

I don't understand the role of OriginalExpr, but I note that the previous L384 added just new_expr, not a TriggerTerm wrapped around new_expr. Is that as intended?

I note that the previous L384 added just new_expr, not a TriggerTerm wrapped around new_expr. Is that as intended?

I'm not sure of what you see but here is the diff I see on my side.

         if (!children_contain_killers) {
           // Add only if the children are not killers; the head has been cleaned up into non-killer form
-          collected_terms.Add(new_term);
+          collected_terms.AddRange(CollectInSetOperations(new_expr, expr));
         }

So it looks like we were previously adding the same thing that I add now, except that now I generate more triggers. Could you elaborate a bit more?

My point was that, previously, collected_terms.Add(new_term); adds new_term, where the new collected_terms.AddRange(CollectInSetOperations(new_expr, expr)); adds

• nothing, or
• new TriggerTerm { Expr = newExpr, OriginalExpr = originalExpr, Variables = CollectVariables(newExpr) } (which is the thing that has a TriggerTerm wrapped around the newExpr), or
• that new TriggerTerm... plus additional triggers.

This is probably fine. I'm just clarifying what I had tried to comment on.

If these are no longer needed, delete the lines. But why are the multiset operations excluded and the set operations still included?

The set operations are still included because there is a flag that can be turned on for sets (aggressive) which is used for frame conditions.
Without these, the tests compiling the Dafny runtime failed, see here
https://github.com/dafny-lang/dafny/actions/runs/4734312552/jobs/8403056164
I found that by reverting this code to its original form, the dafny runtime would verify again. Do you have an idea why?

I was unable to reproduce the failure. However, I think it is correct to omit the multiset operations here, because RewriteInExpr is supposed to be in synch with TrInMultiSet_Aux, which only rewrites MultiSetDisplayExpr.