From a38d47577701beda285f259d17da433fad438ecf Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 17 Oct 2023 16:39:05 +0200
Subject: [PATCH] test: exit 2 in run-kind2.sh when kind2 fails to prove a
property
---
salut/test/bfs-spanning-tree/Makefile | 4 ++--
salut/test/run-kind2.sh | 13 +++++++------
2 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/salut/test/bfs-spanning-tree/Makefile b/salut/test/bfs-spanning-tree/Makefile
index 9b1fa683..75c55583 100644
--- a/salut/test/bfs-spanning-tree/Makefile
+++ b/salut/test/bfs-spanning-tree/Makefile
@@ -11,8 +11,8 @@ include ./Makefile.dot
# Non-regression tests
test: tree13.lurette
- $(RUN_KIND2) tree 3 closure
- $(RUN_KIND2) tree 2 theorem
+ ../run-kind2.sh tree 3 closure
+ ../run-kind2.sh tree 2 ok
clean: genclean
diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh
index 89db6cbf..9b847438 100755
--- a/salut/test/run-kind2.sh
+++ b/salut/test/run-kind2.sh
@@ -54,7 +54,7 @@ kind2 --version || { echo "kind2 is not installed. try: opam install kind2" ; ex
n=$2
main=$1$2
prop=ok
- daemon=daemon_is_distributed
+ daemon=distributed
int=int8
solver=Bitwuzla
shift
@@ -65,7 +65,7 @@ kind2 --version || { echo "kind2 is not installed. try: opam install kind2" ; ex
n=$2
main=$1$2
prop=$3
- daemon=daemon_is_distributed
+ daemon=distributed
int=int8
solver=Bitwuzla
shift
@@ -130,7 +130,7 @@ echo "function daemon<<const an:int; const n:int>> = daemon_is_$daemon<<an,n>>;"
kind2_opt="--timeout 36000 -json -v "
kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
-kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 10000 $@"
+kind2_opt="--exit_code_mode results_and_errors --smt_solver $solver --enable BMC --enable IND --timeout 10000 $@"
# --qe_method {precise|impl|cooper}
@@ -187,7 +187,8 @@ printf "%s %s | %s | %s | %s | %s | %.2f-%.2f | %s | %s | %s | %s |\n" $pb $algo
echo "cf ${ALL_RESULT}"
-if [ -neq $pb "|" ]
- then
- exit 2
+if [ "$pb" = "|" ]; then
+ echo "kind2 proved the property."
+else
+ exit 2
fi
\ No newline at end of file
--
GitLab