At the Gobcon today you mentioned that there could be another attempt at this by you on this, that would be easier to maintain. Could you have a look, whether this indeed exists?

I did a sv-benchmarks run with 60s timeout and here's the CPU time before vs after plot:

On average there's no change to performance but there are some outliers (in both directions!)

All verdict changes except one are close to timeout jitter. One true changes into a quick OUT OF MEMORY which is odd.

I might try looking into some of the biggest outliers before clicking merge.

All verdict changes except one are close to timeout jitter. One true changes into a quick OUT OF MEMORY which is odd.

This task is c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--input--joystick--turbografx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i. Running with -v to see OCaml allocation stats actually shows the memory usage being lower now. This might've just been that slight changes cause GC to trigger a bit later now and there's a moment with higher memory usage.

On average there's no change to performance but there are some outliers (in both directions!)

One of the biggest improvements (2× in time) is on /c/hardware-verification-bv/btor2c-lazyMod.driving_phils.5.prop1-func-interl.c where also the allocated memory amount is halved. This is actually orthogonal to the new deriver: it's just because in this PR I've also replaced the IntDomain hash function with a derived one, which seems to have this huge effect. Maybe the hand-written one has too many collisions or temporary stuff.

In others, e.g. c/goblint-regression/28-race_reach_71-funloop_racing.i there's a slowdown 29s → 36s, which seems to be due to the same hash change. So there seems to be surprisingly large variation in runtime from a single hash function. This might need a separate investigation.