X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu%2Furcu.spin;h=630971f0a280827157bfb19937d7bdbd1d181814;hp=d1aff29fee663d28249a9e608992781741d4e169;hb=86ea30a243222af5ac0860c1b9b1b694a7618f09;hpb=8bc62ca44275eb3dc3f2b62f2ad4a63187473332

diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index d1aff29..630971f 100644
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -264,6 +264,16 @@ inline wait_init_done()
 
 #ifdef TEST_SIGNAL
 
+inline wait_for_sighand_exec()
+{
+	sighand_exec = 0;
+	do
+	:: sighand_exec == 0 -> skip;
+	:: else -> break;
+	od;
+}
+
+#ifdef TOO_BIG_STATE_SPACE
 inline wait_for_sighand_exec()
 {
 	sighand_exec = 0;
@@ -277,6 +287,7 @@ inline wait_for_sighand_exec()
 		fi;
 	od;
 }
+#endif
 
 #else