Multiset domain for recursive must-locksets

[sim642]

1073 introduced multiplicity counters for recursive mutexes in must-locksets. As hinted in https://github.com/goblint/analyzer/pull/1073#discussion_r1217962573, this is simply a multiset domain. However, the implementation keeps a map of multiplicities in addition to the existing must-lockset..

During #1430, which enforces additional correctness via type-safety, numerous unsoundness issues have already been revealed:

1. pthread_mutex_lock(&m[i]); // may lock m[1]
   pthread_mutex_lock(&m[j]); // may lock m[1] recursively
   pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[k]); // may unlock m[0]
   // m[0] should not be in must-lockset here!

2. pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[i]); // may unlock m[0]
   pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[0]); // must unlock m[0]
   // m[0] should not be in must-lockset here!

   (Full regression tests on the mutex-recursive-unsound branch.)

I will fix these in #1430, but a clean multiset-based solution is needed to avoid futher/future instances of unsoundness. The key reason for unsoundness in these cases is that must-locksets have special add and remove behavior: https://github.com/goblint/analyzer/blob/3eee39f9803cff7118c7a8bdbc3f447990d22090/src/cdomains/lockDomain.ml#L42-L56 The Multiplicity map does not, but should. However, duplicating the same logic and keeping it in sync in two data structures is error-prone. A multiset domain would avoid that.

The overhead of storing multiplicity 1 for each non-recursive must-lock is negligible, because it's just one int for each must-lock and our must-locksets are very small.