Something completely mysterious is happening with the fixpoint errors. Printing out the solver solution indicates the unknown being there, yet not being found. Printing hashes shows they match, so that's not the problem. Tracing equal somehow makes the fixpoint error disappear...

Even more mysteriously, at one point duplicating an --enable argument caused the fixpoint error to disappear.

I've hunted the issue down to Apron's compare implementations not being suitable for Set and Make: antoinemine/apron#99. I'm surprised that this hasn't shown up before. Or maybe it has and that's the source of some of the sporadic ERROR (verify) results on sv-benchmarks.

This was for an attempt to validate some witnesses with ghosts. Since we no longer plan to do this and because this didn't scale (or be precise enough, depending on widen), we decided to close this at a GobCon.

I cherry-picked e5f097c and bc85d30 to master.