This hopefully fixes all remaining ERROR (verify) results on sv-benchmarks (Full table).
It is on top of #809 since that causes significant changes to ERROR (verify) results.

Changes

1. CilType.Exp.compare (and also CilType.Exp.equal) previously called CIL's Expcompare.compareExp to check for equality (confusingly not an int compare value) before falling back to the general compare logic implemented there.

   Expcompare.compareExp does some strange things though: it implements only few basic cases and falls back to trying to constant fold both arguments. Such logic is completely inconsistent with everything else in CilType.Exp, which doesn't do similar things for its own compare and hash logic, but which must have consistent behavior.

   In particular, this affected var_eq analysis's expression partition sets, which use compare. The problem is that in non-constant-fold-equal cases the ordering defined by our general logic doesn't account for the equivalences induced by constant folding for equality.

2. All the verify errors in "ufo" benchmarks are about def_exc ranges for booleans. Under some unpredictable conditions, that range could unnecessarily worsen from [0,1] to [0,7].

   The problem seems to be GoblintCil.intKindForValue, which claims

   Return the smallest kind that will hold the integer's value.

   Except it doesn't always return the smallest kind: for 0 and 1 that should be IBool, not IUChar.

   Currently I made the fix in Goblint to quickly debug and benchmark the issue, but it should probably be ported over to CIL.

TODO

• Check if any verify errors remain on sv-benchmarks. No! (Full table)
• Port fix to goblint-cil: Fix intKindForValue for IBool cil#111.
• Fix Gobview after goblint-cil merge for repinning.