Avoid spurious writes for invariants in base mutex-meet-tid

[sim642]

While describing the special invariant writes to globals for my thesis, I looked through all of the write_global implementations and noticed that some mutex-meet variants do not use the optimization:

• base mutex-meet-tid,
• relation mutex-meet,
• relation mutex-meet-tid.

I have quickly added a test for base mutex-meet-tid which reveals precision loss from such spurious side effects. The PR also includes a quick fix for it by analogy, but I haven't thought about it much nor properly tested it.

If this is sound, then we should probably have this since it can improve both precision and performance.

[michael-schwarz]

I'm not sure it is strictly an optimization unfortunately. I think the reason it is not done some of the times is code such as

lock(a);
g = ?;
while(g < 20)  { };
unlock(a);

which occurs quite a few times in SV-COMP snippets as assume_abort_if_not or similar. Here, it may be beneficial to actually consider this a write and later cause a side-effect and add it to LMust.

However, it should still be sound, so maybe we should just try to add it everywhere and then benchmark again?