PR# 10057 Compiler bug for post-condition

If you compile the following code from scratch and press the launch button, you'll see a post-condition violation. Now, uncomment the commented line in 'multiply' feature and re-compile the system (not from scratch) and launch it. The post-condition error does not appear anymore.
============================================
class ROOT_CLASS
create make

feature
	make is
	local
		a, b, r: REAL
	do
		a := 2.2
		b := 5.5
		r := multiply (a, b)
	end

	multiply (num1:REAL; num2: REAL): REAL is
	do
		Result := num1 * num2
--        print ("uncomment this line")	
	ensure
                Result =  num1 * num2 
    end
end

See the description.

Thanks for reporting this. This is a known issue with the backend C compiler which performs comparison with a higher precision than the value stored thus causing the post-condition to fail.