MT94-12-TRIGGER : FLAGMT94-12-TRIGGER is a flag or parameter.
If the current obligation contains fewer than MT94-12-TRIGGER
literals, MT94-12 will behave in the same way as MT94-11
If it contains MT94-12-TRIGGER or more, MT94-12 will choose a literal
with as few mates as possible. There are two extrema: infinity
means that the least branch will only be chosen if the obligation
is as big as the initial obligation; 0 means that the least branch
will always be chosen.
MT94-12-TRIGGER takes values of type INTEGER+-OR-INFINITY.
It belongs to subjects ETREES MTREE-TOP .
Its default value is INFINITY
Its current value is INFINITY.
TPS documentation homepage