those postconditions will never be satisfied
due to
login := a_login.as_string_32 

this is not the same object anymore ...

and the code should be 
create login.make_from_string_general (a_login)