gh verify only 6 randomly

some just take too much time, we would need 1m * 220
and have only 15m

.github/workflows/main.yml

@@ -47,7 +47,7 @@ jobs:
     - uses: actions/checkout@v4
     - run: |
         sudo apt-get -y install cbmc
-    - run: make verify
+    - run: make check-verify
   windows:
     runs-on: windows-latest
     timeout-minutes: 10

GNUmakefile

@@ -61,7 +61,7 @@ else
 endif
 TESTS := $(shell shuf -n 6 good.lst)
 ifeq ($(TESTS),)
-  TESTS = bm mp kmp tbm bom so
+  TESTS = hor mp kmp tbm so ssm
 endif
 
 all: $(BINS) $(HELPERS)
@@ -121,7 +121,7 @@ FAIL = gs tunbm gg rcolussi graspm simon ldm bmh-sbndm faoso4 faoso6 blim \
        bsdm4 bxs fs-w2 fs-w4 fsbndmq32 fsbndmq42 fsbndmq43 fsbndmq62 fsbndmq64 \
        fsbndmq82 fsbndmq84 fsbndmq86 qf26 sbndm-w2 sbndm-w4 tsa tsa-q2 tvsbs-w4 \
        tvsbs-w6 tvsbs-w8 ssecp libc
-TIMEOUT_VERIFY = ag askip aut bsdm2 bm bom2 bom bsdm3 bsdm4 bsdm5 gg gs simon ldm
+TIMEOUT_VERIFY = ag askip aut bsdm2 bm bom2 bom bsdm3 bsdm4 bsdm5 gg gs simon ldm lbndm
 NON_CBMC_SRC   =
 # $(addsuffix .c, $(addprefix source/algos/,$(FAIL_VERIFY)))
 verify:
@@ -131,6 +131,14 @@ verify:
 	  $(TIMEOUT_1m)  cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) $$c || \
             (echo cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) "$$c FAILED"; b=`basename $$c .c`; grep "^$$b.c" good.lst && exit 1); \
 	done
+check-verify:
+	for c in $(addsuffix .c, $(addprefix source/algos/,$(filter-out $(TIMEOUT_VERIFY),$(TESTS)))); \
+	do \
+	  echo $$c; \
+	  echo $(TIMEOUT_1m) cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) $$c; \
+	  $(TIMEOUT_1m)  cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) $$c || \
+            (echo cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) "$$c FAILED"; b=`basename $$c .c`; grep "^$$b.c" good.lst && exit 1); \
+	done
 # prints the violations
 CBMC_ARGS_1 = -DCBMC --depth 1024 --unwind 256 --unwinding-assertions --slice-formula --trace
 verify-trace:

source/algorithms.h

@@ -359,7 +359,7 @@ const struct algo ALGOS[] = {
   [_SBNDM] = {_SBNDM, OK, "sbndm", "Simplified BNDM", 0, 0},
   [_TNDM] = {_TNDM, OK, "tndm", "Two-Way Nondeterministic DAWG Matching", 0, 0},
   [_TNDMa] = {_TNDMa, OK, "tndma", "Two-Way Nondeterministic DAWG Matching (version 2)", 0, 0},
-  [_LBNDM] = {_LBNDM, OK, "lbndm", "long patterns bndm", 0, 0},
+  [_LBNDM] = {_LBNDM, OK, "lbndm", "long patterns bndm", 0, 0}, // TIMEOUT
   // hg BNDM with q-grams
   // bg BNDM with q-grams, and parallel search
   [_SVM0] = {_SVM0, OK, "svm0", "shift vector matching (version 0)", 0, 0},