Bux fix: function is called si2fp and not sitofp.
Bug fix: added declaration of boogie_si_record_float.