Incremental TD3: optimize write-only unknown restarting

[sim642]

On top of #391. This should be a saner version of #633.

This adds a rho_write: S.Dom.t HM.t HM.t data structure, which is used like var_messages, but to retrigger write-only side-effects from superstable unknowns. Ideally, this would also allow collecting all unknown-related messages in rho_write and getting rid of the special var_messages altogether.

To know which unknowns may be treated specially, a is_write_only: t -> bool function is added to the unknowns. This is true for write-only unknowns that are only collected during postsolving, e.g. accesses, but also others.

[sim642]

This somehow screws with compare_runs precision comparisons in the incremental bench. I'll try to look into that before we merge this.

[sim642]

This somehow screws with compare_runs precision comparisons in the incremental bench. I'll try to look into that before we merge this.

Turns out the precision differences were related to severe issues. In particular, the two issues I now fixed caused all or some accesses to disappear even when incrementally analyzing the unchanged program.

This is what happens if all the incremental tests only try to get rid of warnings (which you can do by simply forgetting all of them) and don't check if they are introduced or remain. I added the corresponding -nochange incremental tests to cover the cases I found here.

Precision comparisons on the incremental bench look fine again as well: https://goblint.cs.ut.ee/simmo-results/bench_result-write-only-fixed/. For a couple of basic incremental cases it even fixes the spurious precision difference that came just from a removed access, so the idea seems to work.