function decayAndGetPrice( uint256 id_, uint256 amount_, uint48 time_ ) internal

1. Intended behavior.

   • Adjust the SDA and the pricing of a specific market id.

2. Negative behavior.

   • It shouldn’t be callable whenever

   • It shouldn’t be able to update inactive/ inexistent markets

   • The market capacity shouldn’t overflow/ underflow from the unchecked scope.

3. Preconditions.

   • Assumes the market exists and is functional

   • Assumes adjustments can be made.

4. Postconditions.

   • The totalDebt should be updated (is updated twice)

   • The lastDecay should be updated

   • The metadata[id_].lastDecay should be updated

5. Inputs.

   • id - controllable; amount - controllable: affects the number of payout tokens; block.timestamp - partially controlled

6. Examine all function calls the function makes.

   • There are no external function calls here.