Make privatization sync Join more precise when threadflag is path-sensitive

[sim642]

In #1464, just enabling abortUnless caused two of our simple regression tests in sv-benchmarks to time out:

1. 13-privatized_01-priv_nr_true — This is embarassing...
2. 13-privatized_25-struct_nr_true

Tracing the first one revealed MUTEX_INITS of relational mutex-meet getting additional unwidened increasing side-effects from the body of __VERIFIER_assert, in particular, the join point there. The sync Join which causes these is unnecessary in SV-COMP where threadflag is path-sensitive, so branched thread creation doesn't need to be accounted for by privatizations.

Therefore, this PR makes such privatizations check that and avoid unnecessary side-effects from sync Join. It fixes the two cases, which are probably somewhat outliers that they got an explosion of contexts with abortUnless.
Really, this could make us both more precise (by side-effecting less crap to MUTEX_INITS etc) and more efficient (not modifying MUTEX_INITS which everything depends on).