Fix pretty printer for termination measures

[jcp19]

While pretty printing the Viper files emitted by Gobra, I found two issues with the pretty printer of termination measures:

1. because termination measures are converted into preconditions (posts are also supported, IIRC) by the termination plugin, the pretty printer prints decreases clauses as requires decreases X instead of decreases X
2. When the termination measure is a predicate instance, the PredicateInstance plugin will insert an "@" before the name of the predicate in the termination measure

For a concrete example, viper pretty prints

function IsDuplicableMem(thisItf: Tuple2[Ref, Types]): Bool
  requires decreases @ErrorMem(thisItf)

instead of

function IsDuplicableMem(thisItf: Tuple2[Ref, Types]): Bool
  decreases ErrorMem(thisItf)

PS: I don't understand why predicate instances where being printed with a "@" in the first place, and as far as I can tell, no one relies on this behaviour. Maybe @mschwerhoff knows why.

[marcoeilers]

LGTM. It doesn't look great if the standard silver code refers to a plugin, but IIRC we decided that the termination plugin is supposed to be considered an actual part of silver now, so I think that's fine.

[jcp19]

I was equally apprehensive to make the silver code dependent on a plugin, but having termination checks implemented by a plugin has been a fruitful source of bugs and hacks. I think termination should always have been a part of the language, and I am glad to move in that direction.