invariant(fta.bl==bl);// this is a gratuitous assertion to make sure that the fta struct is still live here. A previous bug but that struct into a C block statement.
invariant(fta.bl==bl);// this is a gratuitous assertion to make sure that the fta struct is still live here. A previous bug put that struct into a C block statement.