remove rule_sanity from 4 rules, and move to 7.17.2

Certora · Nov 20, 2024 · a57b013 · a57b013
1 parent 10b8bdb
commit a57b013
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/.github/workflows/certora-basic.yml b/.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"
diff --git a/.github/workflows/certora-stata.yml b/.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

diff --git a/certora/basic/scripts/run-all.sh b/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"