diff --git a/test/Makefile.inc b/test/Makefile.inc
index 9713d0bf5502fb0d2e13e57a5518f687647c624a..a127186d1d68dd5bf51a2b07420b7fb4c9eb43a1 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -78,8 +78,7 @@ endif
 	sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
 
 # Do not expand nodes 
-%_verify.noexpand.lv4:  verify.lus
-	make $*_const.lus
+%_verify.noexpand.lv4:  verify.lus %_const.lus
 	lv6 $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
 	tac $@ | sed  -z "s/tel/tel\n--%MAIN ;\n--%PROPERTY ok;/" | tac > $@.tmp
 	mv $@.tmp $@
diff --git a/test/kclustering/Makefile b/test/kclustering/Makefile
index 19d67dcfbac589207057995dc4f3a283f65222f7..4e457463a32655d956b591738993567fbea0cf30 100644
--- a/test/kclustering/Makefile
+++ b/test/kclustering/Makefile
@@ -4,8 +4,8 @@ SASA_ALGOS := p.ml
 DECO_PATTERN="0-:p.ml"
 
 
-include ~/sasa/salut/test/Makefile.inc
--include ~/sasa/salut/test/Makefile.dot
+include ../Makefile.inc
+-include ../Makefile.dot
 
 clean: genclean
 	rm -f tree*.*
diff --git a/test/kclustering/verify.lus b/test/kclustering/verify.lus
index 9a5d06e41b0e70293b1f0c0cd0c8cbb6b5baa6a5..702ef10380e1946a1332835d3e36a9b70f49df24 100644
--- a/test/kclustering/verify.lus
+++ b/test/kclustering/verify.lus
@@ -1,5 +1,5 @@
-include "../../sasa/salut/lib/sas.lus"
-include "../../sasa/salut/lib/utils.lus"
+include "../../lib/sas.lus"
+include "../../lib/utils.lus"
 
 include "cost.lus"
 const worst_case=3*card*(card-1)/2 - card - 1;
@@ -12,7 +12,7 @@ returns (ok : bool);
 var
   config : state^card;
   enabled : bool^actions_number^card;
-  legitimate, closure : bool;
+  legitimate, closure,converge : bool;
   steps, cost : int;
 let
 	assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
@@ -22,15 +22,15 @@ let
 	config, enabled = topology(active, init_config);
         assert(config = init_config -> true);
 
-	-- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time
-        legitimate = n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enabled));
+	legitimate = silent<<actions_number,card>>(enabled);
 	closure = true -> (pre(legitimate) => legitimate);
 
         cost = cost(enabled, config);
-       -- converge = (true -> legitimate or pre(cost)>cost);
+       converge = (true -> legitimate or pre(cost)>cost);
 
 	steps = 0 -> (pre(steps) + 1);
 	ok =  closure
+             and converge
      --        and (steps > worst_case) => legitimate      -- the worst-case stabilization
      
      --      and (steps > worst_case - 1) => legitimate  -- is tigth!