Unsound base privatizations after pruning

During benchmarking I found out that some base privatizations can be unsound during witness validation. I've added the following skipped test: https://github.com/goblint/analyzer/blob/e934d115271b7ae4b15e2d25edcf5e22dbcdb7ca/tests/regression/56-witness/04-base-priv-sync-prune.c. The invariant g == 2 should definitely fail, but if run, write+lock currently outputs that it holds.
The same issue occurs with write and lock privatizations separately.

The problem is that these privatizations don't implement sync Join for publishing anything on branched thread creation, but every thread creation loop is a branched thread creation in disguise!
It isn't a problem during the analysis itself, but the postsolving reachability pass never sees enter_multithreaded, so the initial global values are not side-effected and hence are considered unreachable. They are then removed from the solution and when witness validation performs an EvalInt query containing a default bot value, the whole expression comes out as bot, which is the same as if the program point was dead (and the invariant isn't violated).

Therefore these privatizations must also implement sync Join (where there currently are questioning TODOs) in order for the pruned solution to still be sound.

Start with tests/regression/56-witness/04-base-priv-sync-prune.c and run the currently skipped test to reproduce the unsound witness validation. Inspect the write and lock privatizations, especially their existing sync Join TODOs; done means the pruned solution preserves the initial global values and the g == 2 invariant is reported as violated.