[Certora] Liquidate buffer, with executable code

[Certora] Liquidate buffer, with executable code #689