Simmo Saan

I think we never did because we didn't even get it to pass our tests properly, so performance wasn't the primary concern. And we haven't looked at this for a...

I suppose it could also allow optimizing self joins and meets, although I'm not sure how often those really happen. Needs benchmarking to be sure.

> There's some numbers for physical equality in https://github.com/goblint/analyzer/tree/master/bench/hashcons > I still don't know why it doesn't do `a == b || a = b` for `a = b` by...

By the way, other operations like `join` could also be optimized: if the arguments are equal (based on hashconsed tags), then directly return (either) argument. Currently I think we call...

> During the process, it became clear that enhancing protection based with MHP should also be fairly trivial and may also pay off, so we should also take a look...

Could it be that this is also the fault of `WitnessConstraints.PathSensitive3`? Or does this also happen outside of SV-COMP mode? Because it seems weird that the difference is in `var_eq`...

This is weird. I just locally tried all of them under the `svcomp21` tag and they all give `unknown` result instead of `ERROR (verify)`. So I can't even reproduce this...

I can run the same command (with relative paths changed) and get a different result: ``` ./goblint --conf conf/svcomp21.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --html ../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c SV-COMP specification: CHECK( init(main()), LTL(G !...

I don't think it was because I always made the archive build on our Ubuntu 20.04 server where I didn't do any development and also did it after `make clean`....

I will try that soon. It would be quite impossible to debug and fix it though if it somehow doesn't happen on new builds. it might be a hint in...