diff --git a/salut/test/Cycle_unison/Sh/do_org_lines.sh b/salut/test/Cycle_unison/Sh/do_org_lines.sh
deleted file mode 100644
index 36176807fe33b9162c0aa3104d65ec61ac45c1c4..0000000000000000000000000000000000000000
--- a/salut/test/Cycle_unison/Sh/do_org_lines.sh
+++ /dev/null
@@ -1,67 +0,0 @@
-#!/bin/bash
-# Prends en argument k n topologie
-# Exemple : ./search_config.sh 3 7 ring
-
-
-set -x
-if [ $# -ne 3 ]
-    then echo "3 arguments are expected"
-    echo "$0 <k> <n> <topology filename without extension"
-    echo "Exemple : ./search_config.sh 3 7 ring"
-    exit 1
-fi
-
-k=$1
-n=$2
-topology=$3
-log=Log/$topology${k}_$n.log
-
-
-##############################################################
-# building the org table of results using the Log/*.log files
-
-valid=""
-invalid=""
-timeout=""
-stack_overflow=""
-
-grep "ok: valid" $log && valid="true"
-grep "ok: invalid" $log && invalid="true"
-grep "Wallclock timeout" $log && timeout="true"
-grep "Stack overflow" $log && stack_overflow="true"
-
-time=`grep "total runtime" $log | cut -d ' ' -f5`
-
-if [ $valid = "true" ]
-    then resultat="legitimate"
-    step=`grep "ok: " $log | cut -d ' ' -f4 | tr -d ')'`
-fi
-
-if [ "$invalid" = "true" ]
-    then resultat="cycle found"
-    step=`grep "ok: " $log | cut -d ' ' -f4`
-fi
-
-if [ "$timeout" = "true" ]
-    then time="TIMEOUT"
-    step=`grep "ok: " $log | cut -d ' ' -f5`
-fi
-
-if [ "$valid$invalid$timeout" = "" ]
-    then resultat="..."
-fi
-
-# nb: a SO does not mean that kind2 is over
-if  [ "$valid$invalid" = "" -a "$stack_overflow" = "true" ]
-    then resultat="$resultat (SO)"
-fi
-
-
-# d=$(expr $n / 2)
-d=$(expr $n / 2)
-dx2m1=$(expr $d \* 2 - 1)
-dx3m1=$(expr $d \* 3 - 1)
-
-
-echo "| $topology | $k ($dx2m1) | $n | $resultat | $step | $dx3m1 | $time |"  > $log.org
-
diff --git a/salut/test/Cycle_unison/Sh/search_config.sh b/salut/test/Cycle_unison/Sh/search_config.sh
old mode 100644
new mode 100755
index abb8b9a4176e22870e3a9e8bbab8b7efbdafca16..428f7a302f87fc3a0801dfa616802c9b7d4da3a7
--- a/salut/test/Cycle_unison/Sh/search_config.sh
+++ b/salut/test/Cycle_unison/Sh/search_config.sh
@@ -1,50 +1,11 @@
 #!/bin/bash
-# Prends en argument k n topologie
-# Exemple : ./search_config.sh 3 7 ring
-
+# The same as run-kind2, with an extra argument (for generating the k.lus file)
 
 set -x
-if [ $# -ne 3 ]
-    then echo "3 arguments are expected"
-    echo "$0 <k> <n> <topology filename without extension"
-    echo "Exemple : ./search_config.sh 3 7 ring"
-    exit 1
-fi
 
 k=$1
-n=$2
-topology=$3
-log=Log/$topology${k}_$n.log
-
-clean(){
-    rm -f *.cmxs *.cmx *.cmi *.o
-    rm -f $k.ml
-    rm -f *.rif *.seed
-    rm -f $k.lus
-    rm -f *_check_cycles.lv4
-    rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
-    rm -f $k*
-    rm -f k.lus
-}
-
-if [ -z ${LV6OPT} ]; then LV6OPT="" ; fi # n: 194400s = 54 hours
-
-if [ -z ${TIMEOUT} ]; then TIMEOUT=194400.; fi # n: 194400s = 54 hours
+shift
 
-if [ -z ${kind2_opt} ]; then kind2_opt ="--modular true --compositional true"; fi # n: 194400s = 54 hours
-
-clean $3$n
 echo "const k = $k ;" > k.lus
-make $topology$n.dot
-salut $topology$n.dot
-lv6 ${LV6OPT} -eei ${topology}$n.lus check_cycles.lus $topology${n}_const.lus  ../../lib/daemon.lus ../../../test/lustre/round.lus -n check_cycles -rnc --lustre-v4 -o $topology${n}_check_cycles.noexpand.lv4pascal
-cat $topology${n}_check_cycles.noexpand.lv4pascal  | tr '\n' '@' |sed "s/tel@/tel/g" | sed "s/@/\\n/g" | sed "s/tel-- end of node check_cycles/--%MAIN ;\n--%PROPERTY ok;\ntel\n/" | sed "s/telnode/tel\\nnode/" > $topology${n}_check_cycles.noexpand.lv4.tmp
-
-
-mv $topology${n}_check_cycles.noexpand.lv4.tmp $topology${n}_check_cycles.noexpand.lv4
-[ -d Log ] || mkdir Log
-echo "time kind2  --color false ${kind2_opt} $topology${n}_check_cycles.noexpand.lv4"  > $log
-time kind2  --color false ${kind2_opt} $topology${n}_check_cycles.noexpand.lv4 >> $log
 
-##############################################################
-clean $topology$n
+../run-kind2.sh $@
diff --git a/salut/test/Cycle_unison/check_cycles.lus b/salut/test/Cycle_unison/check_cycles.lus
index 52f257ecd3f099a0807f7ba1c6270354b94c4df6..76f4b7725208464d972f92a197fe9f4cea98f44d 100644
--- a/salut/test/Cycle_unison/check_cycles.lus
+++ b/salut/test/Cycle_unison/check_cycles.lus
@@ -1,8 +1,10 @@
 -- include "../../lib/daemon.lus"
 
-node check_cycles(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
+include "daemon_hyp.lus"
+
+node check_cycles(activations : bool^actions_number^card; inits : state^card)
+returns (ok : bool; enables : bool^actions_number^card);
 var config : state^card;
-var enables : bool^actions_number^card;
 
   --  i2 : state^card;
 var legitimate, noloop : bool;
@@ -13,7 +15,7 @@ let
 --  assert(not (legitimate<<actions_number, card>>(enables, inits)));
 
 -- Bad idea in the end
---  assert(not(exists_a_smaller_rot_mir(inits)));
+--  assert(not(exists_a_smaller_rot_mir<<card>>(inits)));
 
   -- not necessary, saves a few percents
 --  assert( --rangei_basic<<card-1>>(inits) and
@@ -22,40 +24,107 @@ let
 --  assert(rangei<<card-1>>(inits));
 
   assert(rangei_alt(inits));
-
-
-  assert(true -> daemon_is_synchronous<<actions_number,card>>(activations, pre enables));
+  assert(true -> daemon<<actions_number,card>>(activations, pre enables));
   assert(true -> inits = pre inits);
 --  inits = inits0 -> pre(inits);
 
   config, enables, lustre_round, lustre_round_nb = topology(activations, inits);
 
   legitimate = legitimate<<actions_number, card>>(enables, config);
+-- When a no cycle exists, it is better (for verification time) to use rot_mir. Otherwise, it isn't.
+  noloop = not (rot_mir<<card>>(inits, config));
 --  noloop = not (inits = config);
--- When a no cycle exists, it is better to use rot_mir. Otherwise, no.
-  noloop = not (rot_mir(inits, config));
   ok = true -> noloop or legitimate;
 tel;
 
-
+-----------------------------------------------------------------------------------
 -- c1 and c2 are equals up to rotation and mirroring
-function rot_mir(c1, c2:state^card) returns (res:bool);
+-- this version uses mirror, which uses concat (which is kind2 un-friendly)
+function rot_mir_concat<<const card:int>>(c1, c2:state^card) returns (res:bool);
 let
-  res = rot(c1,c2) or rot(mirror(c1), c2);
+  res = rot<<card>>(c1,c2) or rot<<card>>(mirror<<card>>(c1), c2);
 tel
-function rot(c1, c2:state^card) returns (res:bool);
+
+-- the same without concat: more involved (and more efficient?)
+function rot_mir<<const card:int>>(c1, c2:state^card) returns (res:bool);
 let
-  res = c1=c2 or rot_rec<<card-1>>(c1,c2);
+  res = rot<<card>>(c1,c2) or rot_mir_i<<card,card>>(c1,c2);
 tel
-function rot_rec<< const N:int>>(c1, c2:state^card) returns (res:bool);
-var c2_rot:state^card;
+node rot_mir5 = rot_mir<<5>>
+
+-- it is the same code as rot, but checking that all possible rot of c2 is a mirror of c1
+function rot_mir_i<< const card:int; const i:int >>(c1, c2:state^card) returns (res:bool);
+let
+  res = with (i=0) then false else
+        rot_mir_i<<card,i-1>>(c1,c2) or rot_mir_i_j<<card, i, card>>(c1,c2);
+tel
+--
+function rot_mir_i_j<< const card:int; const i:int ; const j:int >>
+                     (c1, c2:state^card) returns (res:bool);
+let
+  res = with (j=0) then true else
+          ((c1[(j-1) mod card] = c2[(card+card-j-i) mod card]) -- any rot is a mirror
+      and rot_mir_i_j<<card, i, j-1>>(c1,c2));
+tel
+node check_rot_mir<<const card:int>>(c1, c2:state^card) returns (res:bool);
+let
+  res = (rot_mir_concat<<card>>(c1,c2) = rot_mir<<card>>(c1,c2));
+tel
+node check_rot_mir2 = check_rot_mir<<2>>
+node check_rot_mir3 = check_rot_mir<<3>>
+node check_rot_mir4 = check_rot_mir<<4>>
+node check_rot_mir5 = check_rot_mir<<5>>
+node check_rot_mir6 = check_rot_mir<<6>>
+node check_rot_mir7 = check_rot_mir<<7>>
+node check_rot_mir8 = check_rot_mir<<8>>
+
+-- correct for arrays of size 2 to n
+node check_rot_mir_2<<const n:int>>(c1, c2:state^n) returns (res:bool);
+let
+  res = with n=1 then true else check_rot_mir<<n>>(c1,c2)
+                            and check_rot_mir_2<<n-1>>(c1[0..n-2],c2[0..n-2]);
+tel
+node check_rot_mir_2_10 = check_rot_mir_2<<10>>
+
+(* To verify with kind2 that the 2 rot_mir are equivalent for arrays of size 2 to 10:
+
+ lv6 state.lus check_cycles.lus -n check_rot_mir_2_10 -ec | sed "s/tel/--%MAIN ;\n--%PROPERTY res;\ntel\n/" > checkme.ec
+ kind2 checkme.ec
+*)
+
+-----------------------------------------------------------------------------------
+
+function rot<<const card:int>>(c1, c2:state^card) returns (res:bool);
+let
+  res = rot_i<<card,card>>(c1,c2);
+tel
+function rot_i<< const card:int; const i:int >>(c1, c2:state^card) returns (res:bool);
+let
+  res =
+    with (i=0) then (false)
+               else (rot_i<<card,i-1>>(c1,c2) or rot_i_j<<card, i, card>>(c1,c2));
+tel
+function rot_i_j<< const card:int; const i:int ; const j:int >>(c1, c2:state^card) returns (res:bool);
 let
-  c2_rot = c2[1..card-1] | [c2[0]];
   res =
-    with (N=1) then (c1=c2_rot)
-               else (c1=c2_rot) or rot_rec<<N-1>>(c1,c2_rot);
+    with (j=0) then true
+               else ( (c1[j-1] = c2[(j-1+i) mod card]) and rot_i_j<<card, i, j-1>>(c1,c2));
+tel
+node rot3=rot<<3>>;
+node rot4=rot<<4>>;
+
+(* verify rot is correct
+ lv6 state.lus check_cycles.lus -n check_rot5 -ec | sed "s/tel/--%MAIN ;\n--%PROPERTY res;\ntel\n/" > checkme.ec
+ kind2 checkme.ec
+*)
+node check_rot<<const card:int>>(c1,c2:state^card) returns (res:bool);
+let
+  res = (rot<<card>>(c1,c2) = rot<<card>>(c2,c1));
 tel
+node check_rot5 = check_rot<<5>>;
 
+
+-----------------------------------------------------------------------------------
 function mirror<<const card:int >>(config: state^card) returns (res: state^card);
 let
   res = with (card=1) then [config[0]]
@@ -63,6 +132,31 @@ let
 tel
 
 
+-- nb: is_mirror doesn't use concat, but is more complicated to write
+function is_mirror<<const N:int >>(config, config2: state^N) returns (res: bool);
+let
+  res = is_mirror_do<<N; 0>>(config, config2);
+tel
+function is_mirror_do<<const N:int; const i:int>>(c1, c2: state^N) returns (res: bool);
+let
+  res =
+    with (i=N/2) then (if N mod 2 = 0 then true else c1[N/2]=c2[N/2])
+                 else (c1[i] = c2[N-i-1] and c2[i] = c1[N-i-1] and is_mirror_do<<N, i+1>>(c1,c2));
+
+tel
+node is_mirror4=is_mirror<<4>>;
+node is_mirror5=is_mirror<<5>>;
+
+node check_mirror<<const card:int>>(c1:state^card) returns (res:bool);
+let
+  res = (is_mirror<<5>>(c1,mirror<<card>>(c1)));
+tel
+node check_mirror5 = check_mirror<<5>>;
+
+(* verify that is_mirror is correct (wrt mirror)
+ lv6 state.lus check_cycles.lus -n check_mirror5 -ec | sed "s/tel/--%MAIN ;\n--%PROPERTY res;\ntel\n/" > checkme.ec
+ kind2 checkme.ec
+*)
 -----------------------------------------------------------------------------------
 node rangei4<<const i:int; const k:int>>(c:state^card) returns (res:bool);
 let
@@ -126,7 +220,7 @@ function exists_a_smaller_rot_mir(c1:state^card) returns (res:bool);
 var
   c2 : state^card;
 let
-  c2 = mirror(c1);
+  c2 = mirror<<card>>(c1);
   res = smaller<<card>>(c2, c1) or exists_a_smaller_rot(c1, c1)
                                 or exists_a_smaller_rot(c1, c2);
 tel
diff --git a/salut/test/Makefile b/salut/test/Makefile
index 2f3a3732139030ed15a341a6886187ab68a5f8f5..225fdaa3c2513598bb3018902f4bc86f683c3c8a 100644
--- a/salut/test/Makefile
+++ b/salut/test/Makefile
@@ -26,3 +26,5 @@ compare:
 	cd unison/ && make compare_seed
 	cd bfs-spanning-tree/ && make compare_seed
 	cd rsp_tree/ && make compare_seed
+
+include ./Makefile.local
diff --git a/test/Makefile.inc b/test/Makefile.inc
index ed423c1cc9136e3c089db431cb1635f09c2535b7..c84dcc9c439556944f5ce253015228fc23abca3b 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 23/02/2024 (at 11:18) by Erwan Jahier>
+# Time-stamp: <modified the 15/03/2024 (at 16:36) by Erwan Jahier>
 #
 # Define some default rules that ought to work most of the time
 #
@@ -54,7 +54,6 @@ clean: genclean
 
 ##################################################################################
 #
--include Makefile.untracked
 
 g:gnuplot
 s:sim2chrogtk
diff --git a/test/dune2copy b/test/dune2copy
index 70215208089c9d9c670b32e71b446192ae1f79f7..65f86e1c07065512d034112955267c34b09f6f1a 100644
--- a/test/dune2copy
+++ b/test/dune2copy
@@ -3,57 +3,55 @@
 (library
  (name user_algo_files) ;; a fake name because "%{env:topology=ring4}" is rejected
  (libraries algo)
-; (wrapped false) ; so that user_algo_files is not used in the .cm*
- (library_flags -linkall)
-)
+ ; (wrapped false) ; so that user_algo_files is not used in the .cm*
+ (library_flags -linkall))
 
 ;; copy the <topology>.dot to the build dir if it already exists
 ;; or create it via make otherwise
+
 (rule
- (mode (promote (until-clean)))
+ (mode
+  (promote (until-clean)))
  (target %{env:topology=ring4}.dot)
  (deps
   (:makefile Makefile)
-  (:makefiledot Makefile.dot)
- )
+  (:makefiledot Makefile.dot))
  (action
-  (bash "[ -f ../../%{env:topology=ring4}.dot ] && cp ../../%{env:topology=ring4}.dot . || \
-            make %{env:topology=ring4}.dot")
- )
-)
+  (bash
+   "[ -f ../../%{env:topology=ring4}.dot ] && cp ../../%{env:topology=ring4}.dot . || make %{env:topology=ring4}.dot")))
 
 ;; generate the registration file (out of the dot file)
+
 (rule
  (target %{env:topology=ring4}.ml)
- (deps (:dotfile ./%{env:topology=ring4}.dot))
+ (deps
+  (:dotfile ./%{env:topology=ring4}.dot))
  (action
-  (bash "sasa -reg %{dotfile}")
- )
-)
+  (bash "sasa -reg %{dotfile}")))
 
 (rule
- (mode (promote (until-clean)))
+ (mode
+  (promote (until-clean)))
  (action
   (progn
-    ;; give them back the rigth name
-    (copy user_algo_files.cmxs %{env:topology=ring4}.cmxs)
-    (copy user_algo_files.cmxa  %{env:topology=ring4}.cmxa)
-    (copy user_algo_files.cma  %{env:topology=ring4}.cma)
-    (copy user_algo_files.a  %{env:topology=ring4}.a)
-    ;; we can have only one registering file in the build dir
-    (bash "rm %{env:topology=ring4}.ml")
-   )
- )
- (deps (:src ./%{env:topology=ring4}.dot))
-)
+   ;; give them back the rigth name
+   (copy user_algo_files.cmxs %{env:topology=ring4}.cmxs)
+   (copy user_algo_files.cmxa %{env:topology=ring4}.cmxa)
+   (copy user_algo_files.cma %{env:topology=ring4}.cma)
+   (copy user_algo_files.a %{env:topology=ring4}.a)
+   ;; we can have only one registering file in the build dir
+   (bash "rm %{env:topology=ring4}.ml")))
+ (deps
+  (:src ./%{env:topology=ring4}.dot)))
 
 ;; The glue lustre code between the oracle and the topology
+
 (rule
  (target %{env:topology=ring4}_oracle.lus)
- (mode (promote (until-clean)))
+ (mode
+  (promote (until-clean)))
  (deps
   (:dotfile ./%{env:topology=ring4}.dot)
-  (:cmxs ./%{env:topology=ring4}.cmxs)
-  )
- (action (bash "sasa -glos %{dotfile} -o $(basename $(realpath $PWD/../..))"))
- )
+  (:cmxs ./%{env:topology=ring4}.cmxs))
+ (action
+  (bash "sasa -glos %{dotfile} -o $(basename $(realpath $PWD/../..))")))