Tutorial 8 - invariant doesn't hold in Sparta protocol

[Roy-Certora]

If one tries to check the invariant:
"For both token0 and token1 the balance of the system is at least as much as the reserves.",
in the Sparta pool protocol, one will get failure after invoking the "remove_liquidity" function.
The bug described in the tutorial is fixed by adding a sync() invocation at the beginning of the function,
yet it is not enough to ensure the invariant holds.
My solution was adding a second sync() in the end of "remove_liquidity" as well.

It is probably wise to add the sync() invocation at the end of "swap" as well, to solve the same issue (invariant won't pass).