diff --git a/.gitignore b/.gitignore
index f2fa7fa3..d389275d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,4 @@
 **/emv*
 **/collect.json
 
+.vscode/
\ No newline at end of file
diff --git a/CVLByExample/TransientStorage/Hooks/Mutexer.spec b/CVLByExample/TransientStorage/Hooks/Mutexer.spec
index 0340aac7..ab920429 100644
--- a/CVLByExample/TransientStorage/Hooks/Mutexer.spec
+++ b/CVLByExample/TransientStorage/Hooks/Mutexer.spec
@@ -16,12 +16,21 @@ hook ALL_TSTORE(uint loc, uint v) {
 
 hook ALL_TLOAD(uint loc) uint v {
     if (loc == getContractLock() && executingContract == currentContract) {
-        require contract_lock_status == isLocked(v);
+        require contract_lock_status == isLocked(v), "Match contract lock status";
     }
 }
 
-invariant lockStatusDontChange()
-    !contract_lock_status;
+// invariant version is getting SANITY_FAILURE using the below rule instead
+// invariant lockStatusDontChange()
+//     !contract_lock_status;
+
+rule lockStatusDontChange() {
+    require !contract_lock_status, "Pre condition"; // require contract is not locked
+    // Check that after any method call, the lock is not held
+    method f; env e; calldataarg args;
+    f(e, args);
+    assert !contract_lock_status;
+}
 
 // if contract was locked function call always reverted
 rule checkContractLockReverts(){
diff --git a/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec b/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec
index 08d71c3d..13ef7f6b 100644
--- a/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec
+++ b/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec
@@ -1,6 +1,3 @@
-invariant isUnlocked(env e) 
-   getLock(e) == 0;
-
 invariant deltaZeroWhenUnlocked(env e)
     getLock(e) == 0 => getDelta(e) == 0;
 
@@ -8,7 +5,7 @@ invariant deltaEqualsStorage(env e)
    getDelta(e) == currentContract.storageValue
 {
    preserved onTransactionBoundary with(env e2) {
-      requireInvariant isUnlocked(e2);
+      require getLock(e2) == 0, "Contract must be unlocked";
       requireInvariant deltaZeroWhenUnlocked(e2);
    }
 }
\ No newline at end of file
diff --git a/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec b/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec
index 13fabcc5..226b0ede 100644
--- a/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec
+++ b/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec
@@ -129,12 +129,6 @@ hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
     numOfAccounts[user] = newLength;
 }
 
-/**
- An internal step check to verify that our ghost works as expected, it should mirror the number of accounts.
- Once the sload is defined, this invariant becomes a tautology  
- */
-invariant checkNumOfAccounts(address user) 
-    numOfAccounts[user] == bank.getNumberOfAccounts(user);
 
 /// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances.
 hook Sload uint256 length _customers[KEY address user].accounts.length {
diff --git a/DEFI/ConstantProductPool/contracts/broken/ConstantProductPoolBroken.sol b/DEFI/ConstantProductPool/contracts/broken/ConstantProductPoolBroken.sol
index 4084a231..4369e4d6 100644
--- a/DEFI/ConstantProductPool/contracts/broken/ConstantProductPoolBroken.sol
+++ b/DEFI/ConstantProductPool/contracts/broken/ConstantProductPoolBroken.sol
@@ -38,8 +38,8 @@ contract ConstantProductPool is ERC20 {
     }
 
     constructor(address _token0, address _token1)  {
-        require(token0 != address(0));
-        require(token0 != token1);
+        require(_token0 != address(0));
+        require(_token0 != _token1);
         token0 = _token0;
         token1 = _token1;
         locked = 1;
diff --git a/DEFI/LiquidityPool/certora/specs/Full.spec b/DEFI/LiquidityPool/certora/specs/Full.spec
index 8b9f7e02..cd411b33 100644
--- a/DEFI/LiquidityPool/certora/specs/Full.spec
+++ b/DEFI/LiquidityPool/certora/specs/Full.spec
@@ -441,7 +441,7 @@ rule sharesRoundingTripFavoursContract(env e) {
   prove bug fix
 */
 invariant noClientHasSharesWithMoreValueThanDepositedAmount(address a)
-        sharesToAmount(balanceOf(a)) <= depositedAmount()
+        totalSupply() == 0 || sharesToAmount(balanceOf(a)) <= depositedAmount()
 		{
 			preserved with(env e) {
 				require balanceOf(a) + balanceOf(e.msg.sender) < totalSupply();