Skip to content

Commit

Permalink
Revert "Work-around Z3 bug"
Browse files Browse the repository at this point in the history
This reverts commit b54ec34

I figured out a work-around in CN.
  • Loading branch information
dc-mak committed Aug 26, 2024
1 parent b54ec34 commit fe2d682
Showing 1 changed file with 1 addition and 14 deletions.
15 changes: 1 addition & 14 deletions check.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit fe2d682

Please sign in to comment.