While doing some privatization precision comparisons for #183 using some SV-COMP benchmarks, I saw some differences like:

../sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c:3119 ldv_thread_2: global more precise than global-history
  global: (Unknown int([0,64]))
  more precise than
  global-history: {NULL, ?, &ldv_interrupt_scenario_2@linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c:5238}
  reverse diff: compound: {NULL, ?, &ldv_interrupt_scenario_2@linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c:5238} not same type as (Unknown int([0,64]))

There are cases in ValueDomain.Compound.leq which are somehow supposed to handle the comparison of unknown addresses and unknown integers:

After staring at those cases for a while, trying to understand how they are supposed to fit together, I think I found a case where that leq function isn't even transitive. Consider this snippet:

let v1 = `Int (ID.top_of Cil.IULongLong) in
let v2 = `Address AD.unknown_ptr in
let v3 = `Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) in
ignore (Pretty.printf "v1: %a\n" VD.pretty v1);
ignore (Pretty.printf "v2: %a\n" VD.pretty v2);
ignore (Pretty.printf "v3: %a\n" VD.pretty v3);
ignore (Pretty.printf "v1 leq v2: %B\n" (VD.leq v1 v2));
ignore (Pretty.printf "v2 leq v3: %B\n" (VD.leq v2 v3));
ignore (Pretty.printf "v1 leq v3: %B\n" (VD.leq v1 v3));

It outputs:

v1: (Unknown int([0,64]))
v2: {?}
v3: (Unknown int([-63,63]))
v1 leq v2: true
v2 leq v3: true
v1 leq v3: false

While the non-transitivity (probably) isn't the fault of the initial difference I saw (still looking into it), I now don't know what to make of such comparisons at all.