diff -r ded3f83f6cb9 -r 003cac7b8bf5 no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Mon Jan 06 23:07:51 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Tue Jan 07 22:04:06 2014 +0800
@@ -359,7 +359,7 @@
     and cq2sq: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq s' q = cq2smsgq s q"
     and ffd_remain: "\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> file_of_proc_fd s' p fd = Some f"
     and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags"
-    and sms_remain: "\<forall> q. msgs_of_queue s' q = msgs_of_queue s q"
+    and sms_remain: "\<forall> q. q \<in> current_msgqs s \<longrightarrow> msgs_of_queue s' q = msgs_of_queue s q"
    (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *)
     and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd"
     and nodel: "no_del_event (e # s)"