Test for mutex-meet-tid for ValidDeref & Move Afterconfig.run to ensure privatizations can potentially be auto-tuned

[michael-schwarz]

For tasks such as the example one, we fail to establish Valid-Deref for the reason that our information about globals is too imprecise. With this PR we enable a more involved privatization when checking ValidDeref.

I am currently running this on the server with a reduced timeout of 4mins to see the potential benefits.

[michael-schwarz]

For some reason, the setting is not applied correctly.

./goblint --conf conf/svcomp.json --sets ana.specification /home/michael/Documents/sv-comp/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit 2.c

fails

but

./goblint --conf conf/svcomp.json --sets ana.specification /home/michael/Documents/sv-comp/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit 2.c --set ana.base.privatization mutex-meet-tid

works.

[michael-schwarz]

It seems the autotuner needs to run earlier.

[michael-schwarz]

Enabling the option does not yield a large improvement, and takes a long time. I'll thus remove the activation from this PR.

diff.zip