PR# 19741 Error upon generating clickable view of a feature

Several features that mix class features with agents fail to produce a clickable view, impairing documentation (class clickable and flat view etc.) and, worse, debugging. For example, the three features below, which are presented with their basic text view and with the failed clickable view.

>>>
Basic text view:
	test_flipped
			-- Test {STI_TRANSFORMER}.flipped.
		note
			testing: "covers/{STI_TRANSFORMER}.flipped"
		do
			assert ("flipped", attached {like transformer_to_be_tested}.flipped (agent f_x_acc, some_object_b, some_object_a) implies True)
		end

Clickable view:
	test_flipped
			-- Test {STI_TRANSFORMER}.flipped.
		do
			assert ("flipped", attached {like transformer_to_be_tested}.flipped (agent f_x_acc, some_object_b, some_object_a)Format could not be generated.
Please make sure that the system is not being compiled and that the last compilation was successful.
<<<

>>>
Basic text view:
	singleton_crossed_tuples_ok (
		s: STI_SET [A, EQ]; x: A; ts: STS_SET [STS_N_TUPLE [A, EQ], STS_N_TUPLE_EQUALITY [A, EQ]]
		): BOOLEAN
			-- Do the properties verified within set theory hold for {STI_SET}.singleton_crossed_tuples?
		local
			ns: STI_SET [NATURAL, STS_OBJECT_EQUALITY [NATURAL]]
			m: REAL_64
			l_check: BOOLEAN
		do
			u := u ∪ s & x ∪ {like tuple_to_set}.set_map (ts, agent {STS_N_TUPLE [A, EQ]}.terms).reduced (o, agent {STS_SET [A, EQ]}.united)
			ns := {like tuple_to_natural}.set_map (
				ts, agent (t: STS_N_TUPLE [A, EQ]): NATURAL
					do
						Result := t.n + 1
					end
				)
			m := {like natural_to_real_64}.set_reduction (
				ns, 0, agent (acc: REAL_64; n: NATURAL): REAL_64
					do
						Result := acc + (# u) ^ n
					end
				)
			if m <= Max_tuples then
					if m > Max_asserted_tuples then
						l_check := {ISE_RUNTIME}.check_assert (False)
					end
				check
					definition: s.singleton_crossed_tuples (x, ts) ≍ (
						{like natural_to_tuple_set}.set_reduction (
							ns, ts.o, agent (acc: STS_SET [STS_N_TUPLE [A, EQ], STS_N_TUPLE_EQUALITY [A, EQ]]; n: NATURAL): STS_SET [STS_N_TUPLE [A, EQ], STS_N_TUPLE_EQUALITY [A, EQ]]
								do
									Result := acc ∪ (u ^ n)
								end
							) | agent (t: STS_N_TUPLE [A, EQ]; ia_x: A; ia_ts: STS_SET [STS_N_TUPLE [A, EQ], STS_N_TUPLE_EQUALITY [A, EQ]]): BOOLEAN
								do
									Result := (not t.is_unit and then eq (ia_x, t.first)) and ia_ts ∋ t.tail
								end (?, x, ts)
						)
				then
				end
					if l_check then
						l_check := {ISE_RUNTIME}.check_assert (l_check)
					end
			end

			check
				cardinality: # s.singleton_crossed_tuples (x, ts) = # ts
			then
				Result := True
			end
		ensure
			u: u ≍ old (u ∪ s & x ∪ {like tuple_to_set}.set_map (ts, agent {STS_N_TUPLE [A, EQ]}.terms).reduced (o, agent {STS_SET [A, EQ]}.united))
		end

Clickable view:

	singleton_crossed_tuples_ok (s: STI_SET [A, EQ]; x: A; ts: STS_SET [STS_N_TUPLE [A, EQ], STS_N_TUPLE_EQUALITY [A, EQ]]): BOOLEAN
			-- Do the properties verified within set theory hold for {STI_SET}.singleton_crossed_tuples?
		local
			ns: STI_SET [NATURAL_32, STS_OBJECT_EQUALITY [NATURAL_32]]
			m: REAL_64
			l_check: BOOLEAN
		do
			u := u ∪ s & x ∪ {like tuple_to_set}.set_map (ts, agent {STS_N_TUPLE [A, EQ]}.terms).reduced (o, agent {STS_SET [A, EQ]}.united)
			ns := {like tuple_to_natural}.set_map (ts, agent (t: STS_N_TUPLE [A, EQ]): NATURAL_32
					do
						Result := t.n + 1
					end)
			m := {like natural_to_real_64}.set_reduction (ns, 0.to_double, agent (acc: REAL_64; n: NATURAL_32): REAL_64
					do
						Result := acc + (# u) ^ n.to_real_64
					end)
			if m <= Max_tuples.to_real_64 then
				if m > Max_asserted_tuples.to_real_64 then
					l_check := {ISE_RUNTIME}.check_assert (False)
				end
				check
					definition: s.singleton_crossed_tuples (x, ts)Format could not be generated.
Please make sure that the system is not being compiled and that the last compilation was successful.
<<<

>>>
Basic text view:
	default_create
			-- Create the universe of complex numbers, i.e. ℂ.
		local
			real_numbers, r1, r2: like Real_universe.others
			z: like any_anchor
		do
			from
				others := O
					check
						is_disjoint: R.O.is_disjoint (R) -- R.O.is_empty
					end
				real_numbers := R.O.batch_extended (R)
				r1 := real_numbers
			invariant
				building_up: others ≍{
					TRANSFORMER [
						STS_ORDERED_PAIR [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
						STS_COMPLEX_NUMBER,
						STS_ORDERED_PAIR_EQUALITY [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
						STS_NEW_COMPLEX_EQUALITY
						]
					}.set_map ((R ∖ r1) × R, agent complex_from_pair)
			until
				r1.is_empty
			loop
				from
					r2 := real_numbers
				invariant
					r1_is_not_empty: not r1.is_empty -- Outer loop is not finished.
					still_building_up: others ≍ ({
						TRANSFORMER [
							STS_ORDERED_PAIR [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
							STS_COMPLEX_NUMBER,
							STS_ORDERED_PAIR_EQUALITY [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
							STS_NEW_COMPLEX_EQUALITY
							]
						}.set_map ((R ∖ r1) × R, agent complex_from_pair) ∪ {
						TRANSFORMER [
							STS_ORDERED_PAIR [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
							STS_COMPLEX_NUMBER,
							STS_ORDERED_PAIR_EQUALITY [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
							STS_NEW_COMPLEX_EQUALITY
							]
						}.set_map ({
							TRANSFORMER [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_NEW_REAL_EQUALITY, STS_NEW_REAL_EQUALITY]
							}.singleton_crossed_set (r1.any, R ∖ r2), agent complex_from_pair))
				until
					r2.is_empty
				loop
						check
								-- Loops are not finished.
							r1_is_not_empty: not r1.is_empty
							r2_is_not_empty: not r2.is_empty
						end
					create z.make (r1.any, r2.any)
						check
							does_not_have: others ∌ z -- loop invariant
						end
					others := others.extended (z)
					r2 := r2.others
				variant
					r2_n: natural_as_integer (# r2)
				end
				r1 := r1.others
			variant
				r1_n: natural_as_integer (# r1)
			end
				check
					is_not_empty: not others.is_empty -- not R.is_empty
				end
			z := others.any
			others := others.others
			create any_storage.put (z)
		ensure then
			definition: Current ≍ {
				TRANSFORMER [
					STS_ORDERED_PAIR [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
					STS_COMPLEX_NUMBER,
					STS_ORDERED_PAIR_EQUALITY [STS_REAL_NUMBER, STS_REAL_NUMBER, STS_EQUALITY [STS_REAL_NUMBER], STS_EQUALITY [STS_REAL_NUMBER]],
					STS_NEW_COMPLEX_EQUALITY
					]
				}.set_map (× R, agent complex_from_pair)
		end


Clickable view:
	default_create
			-- Create the universe of complex numbers, i.e. â„‚.
			-- (export status {NONE})
		require -- from  ANY
			True
		local
			real_numbers, r1, r2: like Real_universe.others
			z: like Any_anchor
		do
			from
				others := O
				check
					is_disjoint: R.O.is_disjoint (R)
				end
				real_numbers := R.O.batch_extended (R)
				r1 := real_numbers
			invariant
				building_up: othersFormat could not be generated.
Please make sure that the system is not being compiled and that the last compilation was successful.
<<<

I wasn't able to create a small system where the issue manifests itself. Should I send my entire system for analysis?