8.4.2 Release

8.4.2 Release

640b1a752d6b70f9f7a7dba3992cb399ebbf1573

Author: yoav-el-certora

scripts/certora_cli_publish.py

@@ -178,6 +178,7 @@ def parse_args() -> argparse.Namespace:
     copy(SCRIPTS / "certoraEVMProver.py", CERTORA_CLI_DIR)
     copy(SCRIPTS / "certoraRanger.py", CERTORA_CLI_DIR)
     copy(SCRIPTS / "certoraConcord.py", CERTORA_CLI_DIR)
+    copy(SCRIPTS / "certoraSuiProver.py", CERTORA_CLI_DIR)
     copy(SCRIPTS / "certoraCVLFormatter.py", CERTORA_CLI_DIR)
 
     # write inputs
@@ -256,6 +257,7 @@ def parse_args() -> argparse.Namespace:
             "certoraSorobanProver = certora_cli.certoraSorobanProver:entry_point",
             "certoraEVMProver = certora_cli.certoraEVMProver:entry_point",
             "certoraRanger = certora_cli.certoraRanger:entry_point",
+            "certoraSuiProver = certora_cli.certoraSuiProver:entry_point",
             "certoraCVLFormatter = certora_cli.certoraCVLFormatter:entry_point"
         ]
     }},

scripts/certora_cli_pypi_test.sh

@@ -13,7 +13,7 @@ PACKAGE_NAME="$1"
 VERSION="$2"
 INTERVAL=10 # seconds
 MAX_ATTEMPTS=30
-ENTRY_POINTS=("certoraRun" "certoraMutate" "certoraSolanaProver" "certoraSorobanProver" "certoraEVMProver" "certoraRanger" "certoraConcord" "certoraCVLFormatter")
+ENTRY_POINTS=("certoraRun" "certoraMutate" "certoraSolanaProver" "certoraSorobanProver" "certoraEVMProver" "certoraRanger" "certoraConcord" "certoraCVLFormatter" "certoraSuiProver")
 
 # Print package details
 echo "📦 Package name: $PACKAGE_NAME"

src/main/kotlin/sbf/cfg/SbfCFG.kt

@@ -890,6 +890,12 @@ class MutableSbfCFG(private val name: String): SbfCFG {
             }
             // The basic block has only an unconditional jump to its only successor
             val succB = curB.getMutableSuccs().first()
+
+            if (curB == succB) {
+                // This is an empty loop: we don't touch it.
+                continue
+            }
+
             // Copy predecessors to avoid invalidating iterators
             val predecessors = ArrayList<MutableSbfBasicBlock>(curB.getPreds().size)
             predecessors.addAll(curB.getMutablePreds())