diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 9eb0b4ef308f90e6784e51eadbe4c34fbb872642..8ab4ee60ca741522d565be563559c1224d23022d 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -118,6 +118,9 @@ module Internal  : Domain_builder.InputDomain
 
   type origin = unit (* ???? *)
 
+  let kill loc state =
+    Memory.add_binding ~exact:true state loc V_Or_Uninitialized.top
+
   module Transfer (Valuation:
                      Abstract_domain.Valuation with type value = value
                                                 and type origin = origin
@@ -131,9 +134,6 @@ module Internal  : Domain_builder.InputDomain
 
     let update _valuation st = `Value st (* TODO? *)
 
-    let kill loc state =
-      Memory.add_binding ~exact:true state loc V_Or_Uninitialized.top
-
     let store loc state v =
       let state' =
         match v with
@@ -230,7 +230,10 @@ module Internal  : Domain_builder.InputDomain
   let initialize_variable _ _ ~initialized:_ _ state = state
 
   (* Logic *)
-  let logic_assign _assign _location ~pre:_ _state = top
+  let logic_assign _assign location ~pre:_ state =
+    let loc = Precise_locs.imprecise_location location in
+    kill loc state
+
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index db062fd131da08eab8e7c53b7df3f16bd068c1ff..a447493695dcb04a94297946066499e67a8c077c 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -499,22 +499,23 @@ module CvalueOffsm : Abstract_value.Internal with type t = V.t * offsm_or_top
     else p
 
   (* Refine the value component according to the contents of the offsetmap *)
-  let strengthen_v typ (v, o as p : t) : t =
+  let strengthen_v typ (v, o as p : t) : t or_bottom =
     match o with
-    | Top -> p
+    | Top -> `Value p
     | O o' ->
       let size = size typ in
       (* TODO: this should be done by the transfer function itself... *)
       let v = Cvalue_forward.reinterpret typ v in
       let v_o = V_Or_Uninitialized.get_v (basic_find ~size o') in
       let v_o = Cvalue_forward.reinterpret typ v_o in
-      (V.narrow v v_o, o)
+      let v = V.narrow v v_o in
+      if V.is_bottom v then `Bottom else `Value (v, o)
 
   let forward_unop typ op p =
     match op with
     | BNot ->
       let p' = strengthen_offsm typ p in
-      forward_unop typ op p' >>-: fun p'' ->
+      forward_unop typ op p' >>- fun p'' ->
       strengthen_v typ p''
     | _ -> forward_unop typ op p
 
@@ -523,7 +524,7 @@ module CvalueOffsm : Abstract_value.Internal with type t = V.t * offsm_or_top
     | BAnd | BOr | BXor ->
       let l = strengthen_offsm typ l in
       let r = strengthen_offsm typ r in
-      forward_binop typ op l r >>-: fun p ->
+      forward_binop typ op l r >>- fun p ->
       strengthen_v typ p
     | Shiftlt | Shiftrt ->
       let (v_r, _) = r in
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index 0017418c9fbcf245a0845c9306c4dff7670b008e..b20a057439a25d8d78b9cebdd31242a7f6e83f47 100644
--- a/tests/builtins/diff_bitwise
+++ b/tests/builtins/diff_bitwise
@@ -1,49 +1,304 @@
 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-153,154c153,188
-< [eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze
-< [eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze
----
-> [eva] computing for function analyze <- main.
->   Called from tests/builtins/long_init.c:93.
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] Recording results for analyze
-> [eva] Done for function analyze
-> [eva] computing for function analyze <- main.
->   Called from tests/builtins/long_init.c:94.
-> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-> [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] Recording results for analyze
-> [eva] Done for function analyze
-327c361
+327c327
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_bitwise/Longinit_sequencer.sav
-568c602
+568c568
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_bitwise/Longinit_sequencer.sav
+diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_bitwise/allocated.0.res.oracle
+260a261,263
+> [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
+> [eva:malloc] tests/builtins/allocated.c:127: 
+>   resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
+diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/allocated.1.res.oracle
+191a192,197
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_7}
+208a215,217
+>   strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+223a233,235
+>   strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+238a251,253
+>   strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+254,256d268
+< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+< [eva] tests/builtins/allocated.c:82: 
+<   Call to builtin Frama_C_malloc_fresh for function malloc
+323a336,356
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_31
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_32
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_33
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_34
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_35
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_36
+> [eva] tests/builtins/allocated.c:82: 
+>   Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
+326d358
+< [eva] Semantic level unrolling superposing up to 300 states
+329a362,382
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+399c452,470
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+471c542,560
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+543c632,650
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+615c722,740
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+687c812,830
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+759c902,920
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+831c992,1010
+<   strong free on bases: {__malloc_main_l82_7}
+---
+>   strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87: 
+>   strong free on bases: {__malloc_main_l82_31}
+901,903c1080
+< [eva] tests/builtins/allocated.c:87: Call to builtin free
+< [eva:malloc] tests/builtins/allocated.c:87: 
+<   strong free on bases: {__malloc_main_l82_7}
+---
+> [eva] Semantic level unrolling superposing up to 500 states
+1065,1067c1242,1243
+<   __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
+<                      [1] ∈ {24} or UNINITIALIZED
+<                      [2] ∈ {27} or UNINITIALIZED
+---
+>   __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
+>                      [1] ∈ {17} or UNINITIALIZED
+1136a1313,1333
+>   __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+>   __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
+>                       [1] ∈ {24} or UNINITIALIZED
+>                       [2] ∈ {27} or UNINITIALIZED
+1180c1377
+<   __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
+---
+>   __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
+1203a1401,1407
+>   __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
+>   __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
+1227c1431
+<     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
+---
+>     __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
+1239,1240c1443,1448
+<     __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
+<     __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
+---
+>     __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
+>     __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
+>     __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
+>     __malloc_main_l82_36[0..2]; __malloc_main_l82_37[0..2];
+>     __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
+>     __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
+diff tests/builtins/oracle/malloc-optimistic.res.oracle tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle
+1945a1946,1948
+> [eva] tests/builtins/malloc-optimistic.c:90: Call to builtin malloc
+> [eva:malloc] tests/builtins/malloc-optimistic.c:90: 
+>   resizing variable `__malloc_main7_l90' (0..31/3231) to fit 0..511/3231
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 7803ea7f36d1538b8c338aa8002c10eebd591e1c..10db311b22c2b3ce8099b118afa2d099e5afbc11 100644
--- a/tests/value/bitwise.i
+++ b/tests/value/bitwise.i
@@ -134,6 +134,17 @@ void bug4() {
   }
 }
 
+/* See issue #639 and merge request #2230 on the bitwise domain. */
+void bug5() {
+  int x = v;
+  x = x | 2;
+  if (x == 8) {
+    x = x & 2; /* This branch is dead, but the bitwise domain leads to bottom
+                  only after the operation x&2 and not before. */
+    Frama_C_show_each_dead(x);
+  }
+}
+
 void main(void) {
   test1();
   test2();
@@ -145,4 +156,5 @@ void main(void) {
   bug2();
   bug3();
   bug4();
+  bug5();
 }
diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise
index be860471315a12c865ad8b280eee88bf57f61cda..fbafb12ebb855166d7107c5ac57b6101ed41c0c4 100644
--- a/tests/value/diff_bitwise
+++ b/tests/value/diff_bitwise
@@ -23,6 +23,14 @@ diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.
 <       (origin: Arithmetic {tests/value/addition.i:52}) }}
 ---
 >   p10 ∈ {{ garbled mix of &{p1} }}
+diff tests/value/oracle/bitwise.res.oracle tests/value/oracle_bitwise/bitwise.res.oracle
+79c79,82
+< [eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+---
+> [eva] tests/value/bitwise.i:142: 
+>   The evaluation of the expression x & 2
+>   led to bottom without alarms:
+>   at this point the product of states has no possible concretization.
 diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle
 32,34c32
 < [eva] tests/value/bitwise_pointer.i:18: 
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 29d9bbe232251a10bb728dfe3c9ea3e635cb8fc0..3ec23cec4bf9700c173ea313b5df49bf9bf848b3 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -7,7 +7,7 @@
   input[0..2] ∈ [--..--]
   s ∈ [--..--]
 [eva] computing for function test1 <- main.
-  Called from tests/value/bitwise.i:138.
+  Called from tests/value/bitwise.i:149.
 [eva] computing for function Frama_C_interval <- test1 <- main.
   Called from tests/value/bitwise.i:23.
 [eva] using specification for function Frama_C_interval
@@ -21,18 +21,18 @@
 [eva] Recording results for test1
 [eva] Done for function test1
 [eva] computing for function test2 <- main.
-  Called from tests/value/bitwise.i:139.
+  Called from tests/value/bitwise.i:150.
 [eva] computing for function Frama_C_interval <- test2 <- main.
   Called from tests/value/bitwise.i:50.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for test2
 [eva] Done for function test2
 [eva] computing for function test3 <- main.
-  Called from tests/value/bitwise.i:140.
+  Called from tests/value/bitwise.i:151.
 [eva] Recording results for test3
 [eva] Done for function test3
 [eva] computing for function test4 <- main.
-  Called from tests/value/bitwise.i:141.
+  Called from tests/value/bitwise.i:152.
 [eva] tests/value/bitwise.i:62: assertion got status valid.
 [eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
 [eva] tests/value/bitwise.i:64: 
@@ -45,35 +45,40 @@
 [eva] Recording results for test4
 [eva] Done for function test4
 [eva] computing for function and_or_rel <- main.
-  Called from tests/value/bitwise.i:142.
+  Called from tests/value/bitwise.i:153.
 [eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
 [eva] Recording results for and_or_rel
 [eva] Done for function and_or_rel
 [eva] computing for function double_neg <- main.
-  Called from tests/value/bitwise.i:143.
+  Called from tests/value/bitwise.i:154.
 [eva] Recording results for double_neg
 [eva] Done for function double_neg
 [eva] computing for function bug1 <- main.
-  Called from tests/value/bitwise.i:144.
+  Called from tests/value/bitwise.i:155.
 [eva] Recording results for bug1
 [eva] Done for function bug1
 [eva] computing for function bug2 <- main.
-  Called from tests/value/bitwise.i:145.
+  Called from tests/value/bitwise.i:156.
 [eva] tests/value/bitwise.i:114: Frama_C_show_each_then:
 [eva] tests/value/bitwise.i:114: Frama_C_show_each_else:
 [eva] Recording results for bug2
 [eva] Done for function bug2
 [eva] computing for function bug3 <- main.
-  Called from tests/value/bitwise.i:146.
+  Called from tests/value/bitwise.i:157.
 [eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
 [eva] Recording results for bug3
 [eva] Done for function bug3
 [eva] computing for function bug4 <- main.
-  Called from tests/value/bitwise.i:147.
+  Called from tests/value/bitwise.i:158.
 [eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
 [eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
 [eva] Recording results for bug4
 [eva] Done for function bug4
+[eva] computing for function bug5 <- main.
+  Called from tests/value/bitwise.i:159.
+[eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+[eva] Recording results for bug5
+[eva] Done for function bug5
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -96,6 +101,8 @@
 [eva:final-states] Values at end of function bug4:
   g_2 ∈ {-1; 0}
   tmp_0 ∈ {-0x1578}
+[eva:final-states] Values at end of function bug5:
+  x ∈ [-0x7FFFFFFE..0x7FFFFFFF]
 [eva:final-states] Values at end of function double_neg:
   i ∈ {5}
   j ∈ {0xFFFFFFFA}
@@ -141,6 +148,8 @@
 [from] Done for function bug3
 [from] Computing for function bug4
 [from] Done for function bug4
+[from] Computing for function bug5
+[from] Done for function bug5
 [from] Computing for function double_neg
 [from] Done for function double_neg
 [from] Computing for function test1
@@ -169,6 +178,8 @@
   NO EFFECTS
 [from] Function bug4:
   NO EFFECTS
+[from] Function bug5:
+  NO EFFECTS
 [from] Function double_neg:
   NO EFFECTS
 [from] Function test1:
@@ -202,6 +213,10 @@
     g_2; tmp; tmp_0
 [inout] Inputs for function bug4:
     v
+[inout] Out (internal) for function bug5:
+    x
+[inout] Inputs for function bug5:
+    v
 [inout] Out (internal) for function double_neg:
     i; j; k
 [inout] Inputs for function double_neg: