From b54ec3437ebb4445a81cc82fba9fd8c72d534f6e Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Mon, 26 Aug 2024 14:05:43 +0100
Subject: [PATCH] Work-around Z3 bug

https://github.com/rems-project/cerberus/pull/494 exposed an issue in
the Z3 which is a bit difficult to work around in the implementation
itself and so we have this hacky work-around instead whilst it is fixed
upstream https://github.com/Z3Prover/z3/issues/7352
---
 check.sh | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/check.sh b/check.sh
index 2eb54c26..697d143f 100755
--- a/check.sh
+++ b/check.sh
@@ -14,7 +14,20 @@ good=0
 bad=0
 declare -a bad_tests
 
-for file in $SCRIPT_DIR/src/examples/*c;
+# https://github.com/rems-project/cerberus/pull/494 exposed an issue in
+# the Z3 which is a bit difficult to work around in the implementation
+# itself and so we have this hacky work-around instead whilst it is fixed
+# upstream https://github.com/Z3Prover/z3/issues/7352
+if [[ "${CN}" == "cn verify" ]] \
+    || [[ "${CN}" == *"--solver-type=z3"* ]]; then
+    FILES=($(find "${SCRIPT_DIR}/src/examples" -name '*.c' \
+        ! -name queue_pop.c \
+        ! -name queue_push_induction.c))
+else
+    FILES=($(find "${SCRIPT_DIR}/src/examples" -name '*.c'))
+fi
+
+for file in "${FILES[@]}"
 do
     echo "Checking $file ..."
     $CN $file