From 89025a6bbfc3c4f78af9c1eef2d2ffbf42a86a41 Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Mon, 26 Aug 2024 16:39:08 +0100
Subject: [PATCH] Revert "Work-around Z3 bug"

This reverts commit https://github.com/rems-project/cn-tutorial/commit/b54ec3437ebb4445a81cc82fba9fd8c72d534f6e

I figured out a work-around in CN.
---
 check.sh | 15 +--------------
 1 file changed, 1 insertion(+), 14 deletions(-)

diff --git a/check.sh b/check.sh
index 697d143f..2eb54c26 100755
--- a/check.sh
+++ b/check.sh
@@ -14,20 +14,7 @@ good=0
 bad=0
 declare -a bad_tests
 
-# 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[@]}"
+for file in $SCRIPT_DIR/src/examples/*c;
 do
     echo "Checking $file ..."
     $CN $file