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.

© 1988-99, Carnegie Mellon University.