Closes #367, among other things.

Changes

1. Replace the different reachability, verify, warn, etc post-solving phases with a single top-down (i.e. demand-driven) postsolving phase. This takes the top-down reachability phase, but allows the other features to hook into the same pass over the constraints. This means that all post-solving features use the same right-hand side evaluation instead of repeating it multiple times. This mechanism is flexible enough to allow the side infl collecting of Incremental TD3: restart destabilized side-effected variables #363 to also be integrated into the single postsolving pass.
2. Fix queried and start variable verification (closes Incomplete verify: queried variables are not checked #367). Old Verify2 checked GlobConstrSys, but in the combined mechanism it checks EqConstrSys.
3. Create separate signatures for incremental and non-incremental solvers. Non-incremental solvers are lifted into the incremental signature with no incremental data. This conceptually means that they are also "incremental" but actually solve from scratch.
4. Remove mostly unused Hash module.
5. Fix TD3 modifying Hashtbl during iteration, which according to documentation is undefined behavior. Also add a Semgrep rule to detect such code. This was actually a problem when I tried the same in the new load_run implementation.

TODO

• Check if load_run still works (outputs warnings).

  save_run is now also a postsolver, which marshals the solution to EqConstrSys (not GlobConstrSys), and load_run is a special solver, which just unmarshals the solution. The latter will then run standard postsolvers, including warn to get warnings.

• Adapt compare_runs to changed run marshaling.

  Instead of rewriting Compare for EqConstrSys, I just split their unmarshaled solutions into GlobConstrSys solutions.