Valinity Formal Verification

The floor price is supposed to increase or stay the same after the `tradeOffer()` function call. However, some time can elapse between the creation of an offer and the invocation of `tradeOffer`, which allowes for a scenario where the execution of `tradeOffer()` would bring down the floor price. Let's assume that `createOffer()` was called when the floor price was `x` with `price = 2*x`. Then the floor price increased and went above `2*x`. At this point, when the floor price is greater than `2*x`, if the function `tradeOffer()` is called, it would bring down the value of the floor price. Therefore, it is not possible to formally verify that the floor price is nondecreasing, except by making an assumption that the price at the time of the trade is still above the floor.