Fix syntax errors.

Certora · Dec 13, 2023 · 26d9ea5 · 26d9ea5
1 parent 86b9f66
commit 26d9ea5
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/certora/specs/pool-simple-properties.spec b/certora/specs/pool-simple-properties.spec
@@ -18,7 +18,7 @@ rule method_reachability(env e, method f) {
 
 // @title based on this result of run in the CI:
 // https://prover.certora.com/output/33050/3e09e274b3644f6c9ed051b83a6e4dfb?anonymousKey=b6ade0dd3ada78730183db26a344bafb282861b4
-function methodIsEasyForRuleMethodReachability(method f) returns (bool)
+function methodIsEasyForRuleMethodReachability(method f) returns bool
 {
     return f.isView ||
 	     f.selector == sig:PoolHarness.getUserEMode(address).selector ||
@@ -52,7 +52,7 @@ function methodIsEasyForRuleMethodReachability(method f) returns (bool)
 	     // f.selector == sig:PoolHarness.getReserveStableBorrowRate(address).selector || // view function
 	     // f.selector == sig:PoolHarness.MAX_NUMBER_RESERVES().selector || // view function
 	     // f.selector == sig:PoolHarness.getVariableRateConstant().selector || // view function
-	     f.selector == sig:PoolHarness.configureEModeCategory(uint8,(uint16,uint16,uint16,address,string)).selector ||
+	     f.selector == sig:PoolHarness.configureEModeCategory(uint8,DataTypes.EModeCategory).selector ||
 	     f.selector == sig:PoolHarness.mintToTreasury(address[]).selector ||
 	     f.selector == sig:PoolHarness.updateBridgeProtocolFee(uint256).selector ||
 	     f.selector == sig:PoolHarness.setUserUseReserveAsCollateral(address,bool).selector ||
@@ -72,7 +72,7 @@ function methodIsEasyForRuleMethodReachability(method f) returns (bool)
 	     // f.selector == sig:PoolHarness.getEModeCategoryData(uint8).selector || // view function
 	     f.selector == sig:PoolHarness.BRIDGE_PROTOCOL_FEE().selector ||
 	     // f.selector == sig:PoolHarness.getReserveData(address).selector || // view function
-	     f.selector == sig:PoolHarness.updateReserveIndexes(address).selector ||
+	     f.selector == sig:PoolHarness.updateReserveIndexes(address).selector;
 }
 
 rule method_reachability_split_for_CI_01(env e, method f, calldataarg args) filtered {