X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;fp=formal-model%2Furcu-controldataflow%2Furcu.spin;h=37518685f9360802f5dd405d816c20b389760d5b;hb=e5b00154b490ea239a68244ed245cb888e8eed41;hp=12f841ce46ed7225be2c8fe83b63d938483a00e6;hpb=caeea74ce58faba3ef2bb7d2bd925d9009803086;p=urcu.git

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 12f841c..3751868 100644
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -927,7 +927,7 @@ active proctype urcu_writer()
 	assert(get_pid() < NR_PROCS);
 
 	do
-	:: (loop_nr < 4) ->
+	:: (loop_nr < 3) ->
 #ifdef WRITER_PROGRESS
 progress_writer1:
 #endif