for PR

Author: nisnislevi

.github/workflows/certora-basic.yml

@@ -34,7 +34,7 @@ jobs:
         with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.14.2
+        run: pip install certora-cli==7.17.2
 
       - name: Install solc
         run: |
@@ -70,7 +70,7 @@ jobs:
           - NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
           - NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
           - NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
-          - NEW-pool-simple-properties.conf --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
-          - NEW-pool-simple-properties.conf --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
-          - NEW-pool-simple-properties.conf --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
-          - NEW-pool-simple-properties.conf --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"
+          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
+          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
+          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
+          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"

.github/workflows/certora-stata.yml

@@ -31,7 +31,7 @@ jobs:
         with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.14.2
+        run: pip install certora-cli==7.17.2
       - name: Install solc
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux

certora/basic/scripts/run-all.sh

@@ -1,4 +1,4 @@
-CMN="--compilation_steps_only"
+#CMN="--compilation_steps_only"
 #CMN="--typecheck_only"
 
 
@@ -72,24 +72,28 @@ echo
 echo "******** Running:  simple:6 ***************"
 certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \
            --rule cannotBorrowZeroAmount \
+           --rule_sanity none \
            --msg "simple:6: NEW :: cannotBorrowZeroAmount"
 
 echo
 echo "******** Running:  simple:7 ***************"
 certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \
            --rule cannotBorrowOnInactiveReserve \
+           --rule_sanity none \
            --msg "simple:7: NEW :: cannotBorrowOnInactiveReserve"
 
 echo
 echo "******** Running:  simple:8 ***************"
 certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \
            --rule cannotBorrowOnReserveDisabledForBorrowing \
+           --rule_sanity none \
            --msg "simple:8: NEW :: cannotBorrowOnReserveDisabledForBorrowing"
 
 echo
 echo "******** Running:  simple:9 ***************"
 certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \
            --rule cannotBorrowOnFrozenReserve \
+           --rule_sanity none \
            --msg "simple:9: NEW :: cannotBorrowOnFrozenReserve"