From a57b013e18108342062e38942b57eae346f17ce2 Mon Sep 17 00:00:00 2001
From: nisnislevi <nissan@certora.com>
Date: Wed, 20 Nov 2024 15:40:13 +0200
Subject: [PATCH] remove rule_sanity from 4 rules, and move to 7.17.2

---
 .github/workflows/certora-basic.yml | 10 +++++-----
 .github/workflows/certora-stata.yml |  2 +-
 certora/basic/scripts/run-all.sh    |  6 +++++-
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/certora-basic.yml b/.github/workflows/certora-basic.yml
index 98e04274..c3641210 100644
--- 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
index 370fe36c..4a451edd 100644
--- 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
index 3185e1d3..6d49ffef 100644
--- 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"