I think I see what is going wrong here, but again, I don't know how to fix it.
The postcondition of {EXTERNAL_B}.enlarged_on is being violated because
Result is Void.  Stepping through with the debugger reveals that execution
reaches this line in that function:

  Result ?= byte_node (f, a_type_i).enlarged

The call to `byte_node' returns a non-Void result, but its type is
CONSTANT_B, which does not conform to the type of Result, which is
CALL_ACCESS_B.  

Without knowing anything about how the code works, I thought perhaps
the return type should instead be ACCESS_B, but making that change
causes a cascade of "redeclaration has non-conforming signature" validity
errors, so I gave up at that point.

Maybe you already know all that and there is no simple localized fix.