`rel` Expressions in Triggers

[ArquintL]

The SIF plugin seems to correctly encode rel expressions appearing in quantifier bodies but does not encode such expressions appearing in triggers, which, thus, results in a RuntimeException during verification.

However, this issue seems to depend on the surrounding expression. In particular assert forall _ { rel(_,1) } _ seems to get encoded while inhale forall _ { rel(_,1) } _ does not. See Gobra #987 for an example input.

[marcoeilers]

The AST node for rel-expressions is currently marked as not allowed in triggers at all, any quantifier using it in a trigger should actually be rejected by a consistency check. So I cannot actually write a Viper program where the encoding problem shows up.

This might be the one consistency check that is performed only after the translation from ParseAST to AST, which would mean that it isn't done when using Viper from a frontend. I'll have a look at that, that would obviously be something we should fix.

But independently of that: What's the use case for using rel inside a trigger? If this is useful at least sometimes, we should probably officially allow it (and then fix any errors that show up).