diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
index f9d852b3..653eaff1 100644
--- a/runStableTokenCLI.sh
+++ b/runStableTokenCLI.sh
@@ -1 +1 @@
-certoraRun.py specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
\ No newline at end of file
+certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --staging
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index 16fed3bb..a486d335 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -36,7 +36,7 @@ rule balanceOfChange(address a, address b, method f)
 }
 
 /**
-Checks that the change to total supply is coherent with the change to balance due to an operation
+Checks that the change to total supply is coherent with the change to user balance due to an operation
 (which is not burn).
 */
 rule integirtyBalanceOfTotalSupply(address a, method f )
@@ -55,24 +55,49 @@ rule integirtyBalanceOfTotalSupply(address a, method f )
 	assert  (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
+
 /**
-Burn behaves differently and due to accumulation errors might have less total supply than the balance.
+Checks that the change to total supply is coherent with the change to user balance due to a burn operation.
 */
-rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
+rule integirtyBalanceOfTotalSupplyOnBurn(address a, uint256 x)
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
+	
 	uint256 balanceABefore = sinvoke balanceOf(e, a);
+	
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
-	 
-	uint256 x;
+	uint256 averageStableRateBefore = sinvoke getAverageStableRate(e);
+	uint256 debtSupplyBefore = sinvoke rayWadMul(e, averageStableRateBefore, totalSupplyBefore);
+	
+	uint256 stableRateA = sinvoke getUserStableRate(e, a);
+	uint256 repaidDebtA = sinvoke rayWadMul(e, stableRateA, x);
+	
+	
 	sinvoke burn(e, a, x); 
 	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
-	if (totalSupplyBefore > x)
-		assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
-	else
+
+	if(totalSupplyBefore > x) {
+	    /* The amount being burned (x) is smaller than the total supply */
+		if(repaidDebtA >= debtSupplyBefore) {
+			/*
+			The user debt being repaid is at least the debt supply.
+			The total supply becomes 0.
+			*/
+			assert(totalSupplyAfter == 0);
+		}
+		else {
+			assert(balanceAAfter != balanceABefore  =>
+			(balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+		}
+	}
+	else {
+	/* The amount being burned (x) is at least the total supply.
+	   The total supply becomes 0.
+	*/
 		assert (totalSupplyAfter == 0);
+	}
 }
 
 /**
diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol
index 69a9aa8a..6a8323ca 100644
--- a/specs/harness/StableDebtTokenHarness.sol
+++ b/specs/harness/StableDebtTokenHarness.sol
@@ -11,7 +11,11 @@ contract StableDebtTokenHarness is StableDebtToken {
     string memory symbol,
     address incentivesController
   ) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
-
+	
+	
+   /**
+   Simplification: The user accumulates no interest (the balance increase is always 0).
+   **/
   function balanceOf(address account) public override view returns (uint256) {
     return IncentivizedERC20.balanceOf(account);
   }
@@ -23,4 +27,8 @@ contract StableDebtTokenHarness is StableDebtToken {
   function getIncentivesController() public view returns (address) {
     return address(_incentivesController);
   }
+  
+  function rayWadMul(uint256 aRay, uint256 bWad) external view returns(uint256) {
+	return aRay.rayMul(bWad.wadToRay());
+  }
 }