test: exit 2 in run-kind2.sh when kind2 fails to prove a property

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

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