diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index a98c8c40fee00a07cde4017134532cf00c085725..e1afac0cf11fb77ae6e5dc5fd1e27eb7692a8480 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -660,6 +660,8 @@ end
 
 module type BitOperator =
 sig
+  (* Concrete version of the bitwise operator *)
+  val concrete_bitwise : Int.t -> Int.t -> Int.t
   (* Printable version of the operator *)
   val representation : string
   (* forward is given here as the lifted function of some bit operator op
@@ -682,6 +684,8 @@ end
 
 module And : BitOperator =
 struct
+  let concrete_bitwise = Int.logand
+
   let representation = "&"
 
   let forward v1 v2 =
@@ -701,6 +705,8 @@ end
 
 module Or : BitOperator =
 struct
+  let concrete_bitwise = Int.logor
+
   let representation = "|"
 
   let forward v1 v2 =
@@ -720,6 +726,8 @@ end
 
 module Xor : BitOperator =
 struct
+  let concrete_bitwise = Int.logxor
+
   let representation = "^"
 
   let forward v1 v2 =
@@ -893,7 +901,15 @@ struct
       acc := List.fold_left (set_bit (Bit i)) [] !acc;
       if List.length !acc > small_cardinal () then raise Do_not_fit_small_sets
     done;
-    let list = List.map (fun (r, _, _) -> r) !acc in
+    (* Keep only values that can actually be obtained *)
+    let is_admissible (r, v1, v2) =
+      match v1, v2 with
+      | Set s1, Set s2 ->
+        let op = Op.concrete_bitwise in
+        Int_set.(exists (fun i1 -> exists (fun i2 -> op i1 i2 = r) s2) s1)
+      | _, _ -> true
+    in
+    let list = Extlib.filter_map is_admissible (fun (r, _, _) -> r) !acc in
     Set (Int_set.inject_list list)
 
   (* If lower is true (resp. false), compute the lower (resp. upper) bound of
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 10db311b22c2b3ce8099b118afa2d099e5afbc11..92a3bc59753007005c262734211c8a2d0d8f4aa6 100644
--- a/tests/value/bitwise.i
+++ b/tests/value/bitwise.i
@@ -2,11 +2,16 @@
    STDOPT: +"-big-ints-hex 256"
 */
 
-/*@ assigns \result \from min, max;
-    ensures min <= \result <= max ;
+/*@ assigns \result \from a, b;
+    ensures result_a_or_b: \result == a || \result == b ;
  */
-int Frama_C_interval(int min, int max);
+extern int Frama_C_nondet(int a, int b);
 
+/*@ requires order: min <= max;
+    assigns \result \from min, max;
+    ensures result_bounded: min <= \result <= max ;
+ */
+extern int Frama_C_interval(int min, int max);
 
 volatile long v;
 volatile unsigned char input[3];
@@ -67,13 +72,22 @@ int test4(void)
   if (something & 0x80000000) {
     Frama_C_show_each_true(something);
     return 0;
-  } 
+  }
   else {
     Frama_C_show_each_false(something);
     return 1;
   }
 }
 
+void test5(void)
+{
+  int x = Frama_C_nondet(-1, 0);
+  int y = Frama_C_nondet(-1, 0);
+  int a = x & y;
+  int b = x | y;
+  int c = x ^ y;
+}
+
 void and_or_rel(void)
 {
   long x, r1, r2, r3;
@@ -150,6 +164,7 @@ void main(void) {
   test2();
   test3();
   test4();
+  test5();
   and_or_rel();
   double_neg();
   bug1();
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 5bd9c79813b7339a8da28995f913223872b77d97..20f6783fe6514a1335d5f58836344cf7e4ee34e3 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -7,76 +7,95 @@
   input[0..2] ∈ [--..--]
   s ∈ [--..--]
 [eva] computing for function test1 <- main.
-  Called from tests/value/bitwise.i:149.
+  Called from tests/value/bitwise.i:163.
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:23.
+  Called from tests/value/bitwise.i:28.
 [eva] using specification for function Frama_C_interval
+[eva] tests/value/bitwise.i:28: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:24.
+  Called from tests/value/bitwise.i:29.
+[eva] tests/value/bitwise.i:29: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:25.
+  Called from tests/value/bitwise.i:30.
+[eva] tests/value/bitwise.i:30: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for test1
 [eva] Done for function test1
 [eva] computing for function test2 <- main.
-  Called from tests/value/bitwise.i:150.
+  Called from tests/value/bitwise.i:164.
 [eva] computing for function Frama_C_interval <- test2 <- main.
-  Called from tests/value/bitwise.i:50.
+  Called from tests/value/bitwise.i:55.
+[eva] tests/value/bitwise.i:55: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [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:151.
+  Called from tests/value/bitwise.i:165.
 [eva] Recording results for test3
 [eva] Done for function test3
 [eva] computing for function test4 <- main.
-  Called from tests/value/bitwise.i:152.
-[eva] tests/value/bitwise.i:62: assertion got status valid.
-[eva] tests/value/bitwise.i:64: 
+  Called from tests/value/bitwise.i:166.
+[eva] tests/value/bitwise.i:67: assertion got status valid.
+[eva] tests/value/bitwise.i:69: 
   Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
-[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
-[eva] tests/value/bitwise.i:66: 
+[eva] tests/value/bitwise.i:69: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
+[eva] tests/value/bitwise.i:71: 
   Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
-[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
-[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
-[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:71: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
+[eva] tests/value/bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
 [eva] Recording results for test4
 [eva] Done for function test4
+[eva] computing for function test5 <- main.
+  Called from tests/value/bitwise.i:167.
+[eva] computing for function Frama_C_nondet <- test5 <- main.
+  Called from tests/value/bitwise.i:84.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] computing for function Frama_C_nondet <- test5 <- main.
+  Called from tests/value/bitwise.i:85.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for test5
+[eva] Done for function test5
 [eva] computing for function and_or_rel <- main.
-  Called from tests/value/bitwise.i:153.
-[eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
+  Called from tests/value/bitwise.i:168.
+[eva:alarm] tests/value/bitwise.i:101: 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:154.
+  Called from tests/value/bitwise.i:169.
 [eva] Recording results for double_neg
 [eva] Done for function double_neg
 [eva] computing for function bug1 <- main.
-  Called from tests/value/bitwise.i:155.
+  Called from tests/value/bitwise.i:170.
 [eva] Recording results for bug1
 [eva] Done for function bug1
 [eva] computing for function bug2 <- main.
-  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:
+  Called from tests/value/bitwise.i:171.
+[eva] tests/value/bitwise.i:128: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:128: 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:157.
-[eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
+  Called from tests/value/bitwise.i:172.
+[eva] tests/value/bitwise.i:135: 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:158.
-[eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
+  Called from tests/value/bitwise.i:173.
+[eva] tests/value/bitwise.i:145: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:147: 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}
+  Called from tests/value/bitwise.i:174.
+[eva] tests/value/bitwise.i:158: Frama_C_show_each_dead: {0}
 [eva] Recording results for bug5
 [eva] Done for function bug5
 [eva] Recording results for main
@@ -136,6 +155,12 @@
   something ∈ [0..0x7FFFFFFF]
   topBitOnly ∈ {0; 0x80000000}
   __retres ∈ {1}
+[eva:final-states] Values at end of function test5:
+  x ∈ {-1; 0}
+  y ∈ {-1; 0}
+  a ∈ {-1; 0}
+  b ∈ {-1; 0}
+  c ∈ {-1; 0}
 [eva:final-states] Values at end of function main:
   
 [from] Computing for function and_or_rel
@@ -162,12 +187,18 @@
 [from] Done for function test3
 [from] Computing for function test4
 [from] Done for function test4
+[from] Computing for function test5
+[from] Computing for function Frama_C_nondet <-test5
+[from] Done for function Frama_C_nondet
+[from] Done for function test5
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function Frama_C_interval:
   \result FROM min; max
+[from] Function Frama_C_nondet:
+  \result FROM a; b
 [from] Function and_or_rel:
   NO EFFECTS
 [from] Function bug1:
@@ -190,6 +221,8 @@
   NO EFFECTS
 [from] Function test4:
   \result FROM v
+[from] Function test5:
+  NO EFFECTS
 [from] Function main:
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
@@ -238,6 +271,10 @@
     something; topBitOnly; __retres
 [inout] Inputs for function test4:
     v
+[inout] Out (internal) for function test5:
+    x; y; a; b; c
+[inout] Inputs for function test5:
+    \nothing
 [inout] Out (internal) for function main:
     \nothing
 [inout] Inputs for function main: