diff --git a/tests/regression/27-inv_invariants/20-union-map-domain-float-int.c b/tests/regression/27-inv_invariants/20-union-map-domain-float-int.c new file mode 100644 index 0000000000..40ff1d77da --- /dev/null +++ b/tests/regression/27-inv_invariants/20-union-map-domain-float-int.c @@ -0,0 +1,28 @@ +// PARAM: --enable ana.float.interval --set ana.base.unions.domain map +#include +union u { + int x; + float f; +}; + +int main(){ + union u a; + union u b; + + a.x = 12; + b.f = 129.0; + + int i = 0; + if(a.x == b.x){ + i++; + } + // Should not be dead after if + __goblint_check(1); + + if(a.f == b.f){ + i++; + } + // Should not be dead after if + __goblint_check(1); + return 0; +}