From 0af219f63aee2cb3e7c55cae464bcba3e2c31f98 Mon Sep 17 00:00:00 2001
From: Reini Urban <reini.urban@gmail.com>
Date: Fri, 29 Mar 2024 20:53:04 +0100
Subject: [PATCH] gh verify only 6 randomly

some just take too much time, we would need 1m * 220
and have only 15m
---
 .github/workflows/main.yml |  2 +-
 GNUmakefile                | 12 ++++++++++--
 source/algorithms.h        |  2 +-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 2d969d63..4845883e 100644
--- a/.github/workflows/main.yml
+++ b/.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
diff --git a/GNUmakefile b/GNUmakefile
index d5e51974..fa5aa2c9 100644
--- a/GNUmakefile
+++ b/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:
diff --git a/source/algorithms.h b/source/algorithms.h
index c92dd678..a7c1d4ca 100644
--- a/source/algorithms.h
+++ b/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},