Add disjunctive completion of Apron domains

[sim642]

This is on top of #1216 as an attempt to make it handle disjunctive relational invariants.

It "works" except there are some very odd fixpoint errors that I'll have to debug further. Last I looked at them it seemed so odd that they might've something to do with the mutable aspects of Apron domains.

[sim642]

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.

[sim642]

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.

[sim642]

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.