Summary

sender transferring their funds state variables is not updated.

Vulnerability Details

a user can make multiple transfers of the same amount without decreasing the sender balance. The invariant test fails if you check balance before
transfer and balance after transfer of sender because is still the same amount

Impact

funds can be drained from contract. This can cause a DOS for other user when they try to transfer or withdraw

Tools Used

manual, fuzz testing

Recommendations

decrease the sender amount before the transfers.