If DEEPEST, the default next obligation is found by depth-first

search of the obtree, if HIGHEST it is found by breadth-first-search,

if D-SMALLEST then the deepest of the set of smallest obligations (i.e.

the set of all obligations with the fewest possible literals) is

chosen, if H-SMALLEST then the highest of this set is chosen.

DEFAULT-OB takes values of type OBDEFAULT.

It belongs to subjects ETREES MTREE-TOP .

Its default value is D-SMALLEST

Its current value is D-SMALLEST.

© 1988-99, Carnegie Mellon University.