diff --git a/specs/UserConfiguration.spec b/specs/UserConfiguration.spec
index 14fce3a6..41a4f93e 100644
--- a/specs/UserConfiguration.spec
+++ b/specs/UserConfiguration.spec
@@ -1,66 +1,66 @@
 methods {
-	setBorrowing(address, uint256, bool) envfree
-	setUsingAsCollateral(address, uint256, bool) envfree
-	isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree
-	isBorrowing(address, uint256) returns bool envfree
-	isUsingAsCollateral(address, uint256) returns bool envfree
-	isBorrowingAny(address ) returns bool envfree
- 	isEmpty(address ) returns bool envfree
+	setBorrowing(uint256, bool) envfree
+	setUsingAsCollateral(uint256, bool) envfree
+	isUsingAsCollateralOrBorrowing(uint256) returns bool envfree
+	isBorrowing(uint256) returns bool envfree
+	isUsingAsCollateral(uint256) returns bool envfree
+	isBorrowingAny() returns bool envfree
+ 	isEmpty() returns bool envfree
 }
 
-invariant empty(address user, uint256 reserveIndex ) 
-	 isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
+invariant empty(uint256 reserveIndex) 
+	 isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex)
 
-invariant notEmpty(address user, uint256 reserveIndex ) 
-	( isBorrowingAny(user) ||  isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
+invariant notEmpty(uint256 reserveIndex) 
+	(isBorrowingAny() ||  isUsingAsCollateral(reserveIndex)) => !isEmpty()
 
 
-invariant borrowing(address user, uint256 reserveIndex ) 
-	 isBorrowing(user, reserveIndex) =>  isBorrowingAny(user) 
+invariant borrowing(uint256 reserveIndex ) 
+	 isBorrowing(reserveIndex) =>  isBorrowingAny() 
 
-invariant collateralOrBorrowing(address user, uint256 reserveIndex ) 
-	( isUsingAsCollateral(user, reserveIndex) ||  isBorrowing(user, reserveIndex) ) <=>  isUsingAsCollateralOrBorrowing(user, reserveIndex) 
+invariant collateralOrBorrowing(uint256 reserveIndex ) 
+	(isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=>  isUsingAsCollateralOrBorrowing(reserveIndex) 
 
 
 
-rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
+rule setBorrowing(uint256 reserveIndex, bool borrowing)
 {
 	require reserveIndex < 128;
 	
-	setBorrowing(user, reserveIndex, borrowing);
-	assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
+	setBorrowing(reserveIndex, borrowing);
+	assert isBorrowing(reserveIndex) == borrowing, "unexpected result";
 }
 
-rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
+rule setBorrowingNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
 {
 	require reserveIndexOther != reserveIndex;
 	require reserveIndexOther < 128 && reserveIndex < 128;
-	bool otherReserveBorrowing =  isBorrowing(user, reserveIndexOther);
-	bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
+	bool otherReserveBorrowing =  isBorrowing(reserveIndexOther);
+	bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
 
-	setBorrowing(user, reserveIndex, borrowing);
-	assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
-		otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
+	setBorrowing(reserveIndex, borrowing);
+	assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
+		otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
 }
 
 
-rule  setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
+rule  setUsingAsCollateral(uint256 reserveIndex, bool usingAsCollateral)
 {
 	require reserveIndex < 128;
 	
-	setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
-	assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
+	setUsingAsCollateral(reserveIndex, usingAsCollateral);
+	assert isUsingAsCollateral(reserveIndex) == usingAsCollateral, "unexpected result";
 }
 
 
-rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
+rule setUsingAsCollateralNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
 {
 	require reserveIndexOther != reserveIndex;
 	require reserveIndexOther < 128 && reserveIndex < 128;
-	bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
-	bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
+	bool otherReserveBorrowing = isBorrowing(reserveIndexOther);
+	bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther);
 	
-	setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
-	assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
-		otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
+	setUsingAsCollateral(reserveIndex, usingAsCollateral);
+	assert otherReserveBorrowing == isBorrowing(reserveIndexOther) &&
+		otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve";
 }
diff --git a/specs/harness/UserConfigurationHarness.sol b/specs/harness/UserConfigurationHarness.sol
index 00a8da90..4487773b 100644
--- a/specs/harness/UserConfigurationHarness.sol
+++ b/specs/harness/UserConfigurationHarness.sol
@@ -2,15 +2,16 @@ pragma solidity 0.6.12;
 pragma experimental ABIEncoderV2;
 
 import {UserConfiguration} from '../../contracts/protocol/libraries/configuration/UserConfiguration.sol';
+import {DataTypes} from '../../contracts/protocol/libraries/types/DataTypes.sol';
 
 /*
 A wrapper contract for calling functions from the library UserConfiguration.
 */
 contract UserConfigurationHarness {
+
   DataTypes.UserConfigurationMap internal usersConfig;
 
   function setBorrowing(
-    address user,
     uint256 reserveIndex,
     bool borrowing
   ) public {
@@ -18,14 +19,13 @@ contract UserConfigurationHarness {
   }
 
   function setUsingAsCollateral(
-    address user,
     uint256 reserveIndex,
     bool _usingAsCollateral
   ) public {
     UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
   }
 
-  function isUsingAsCollateralOrBorrowing(address user, uint256 reserveIndex)
+  function isUsingAsCollateralOrBorrowing(uint256 reserveIndex)
     public
     view
     returns (bool)
@@ -33,19 +33,19 @@ contract UserConfigurationHarness {
     return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
   }
 
-  function isBorrowing(address user, uint256 reserveIndex) public view returns (bool) {
+  function isBorrowing(uint256 reserveIndex) public view returns (bool) {
     return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
   }
 
-  function isUsingAsCollateral(address user, uint256 reserveIndex) public view returns (bool) {
+  function isUsingAsCollateral(uint256 reserveIndex) public view returns (bool) {
     return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
   }
 
-  function isBorrowingAny(address user) public view returns (bool) {
+  function isBorrowingAny() public view returns (bool) {
     return UserConfiguration.isBorrowingAny(usersConfig);
   }
 
-  function isEmpty(address user) public view returns (bool) {
+  function isEmpty() public view returns (bool) {
     return UserConfiguration.isEmpty(usersConfig);
   }