This issue contains all modifications made to B model for proof activities without functional impact.