diff --git a/src/plugins/wp/tests/wp_bts/bts_2110.i b/src/plugins/wp/tests/wp_bts/bts_2110.i
index 807a50f5053ba69291bc3408ccd85bad69fb88a7..c3e92f41a345f65ee05065f318116fe741cf69c1 100644
--- a/src/plugins/wp/tests/wp_bts/bts_2110.i
+++ b/src/plugins/wp/tests/wp_bts/bts_2110.i
@@ -8,30 +8,23 @@
 */
 
 struct FD {
-	int pos;
-	int *adr;
+  int pos;
+  int *adr;
 };
 
 struct A { int dummy; };
 
 /*@
-	//requires \valid(fd);
-	//requires \valid(a);
-	//requires \separated(a,fd);
-	assigns fd->pos;
-	assigns *a;
-	ensures fd->pos != \old(fd->pos);
+  assigns fd->pos;
+  assigns *a;
+  ensures fd->pos != \old(fd->pos);
 */
 int myRead(struct FD* fd,struct A* a);
 
 /*@
-	//requires \valid(fd);
-	//requires \valid(a);
-	//requires \separated(a,fd);
-	ensures KO: *a == \old(*a);
+  ensures KO: *a == \old(*a);
 */
 void myMain(struct FD* fd,struct A* a)
 {
-	//@ assigns KO: *a;
-	myRead(fd,a);
+  myRead(fd,a);
 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index ccaf0802ca728955534bc9243cd74a446b58e60b..29356cc19ac00c18539f191f8aff775a43c78808 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing tests/wp_bts/bts_2110.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] 1 goal scheduled
 ---------------------------------------------
 --- Context 'typed_myMain' Cluster 'S2_A' 
 ---------------------------------------------
@@ -50,8 +50,6 @@ theory Compound
   
   (* use frama_c_wp.memory.Memory *)
   
-  function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0
-  
   function shiftfield_F2_A_dummy (p:addr) : addr = shift p 0
   
   (* use S2_A *)
@@ -59,6 +57,8 @@ theory Compound
   function Load_S2_A (p:addr) (mint:addr -> int) : S2_A =
     S2_A1 (get mint (shiftfield_F2_A_dummy p))
   
+  function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0
+  
   Q_Load_S2_A_update_Mint0 :
     forall mint:addr -> int, p:addr, q:addr, v:int
      [Load_S2_A p (set mint q v)].
@@ -95,43 +95,17 @@ end
     
     (* use frama_c_wp.memory.Memory *)
     
-    (* use S2_A *)
-    
-    (* use Compound *)
-    
-    goal wp_goal :
-      forall t:addr -> int, t1:addr -> int, a:addr.
-       let a1 = Load_S2_A a t in
-       let a2 = Load_S2_A a (havoc t1 t a 1) in
-       region (base a) <= 0 -> IsS2_A a1 -> IsS2_A a2 -> EqS2_A a2 a1
-  end
-[wp:print-generated] 
-  theory WP1
-    (* use why3.BuiltIn.BuiltIn *)
-    
-    (* use bool.Bool *)
-    
-    (* use int.Int *)
-    
-    (* use int.ComputerDivision *)
-    
-    (* use real.RealInfix *)
-    
-    (* use frama_c_wp.qed.Qed *)
-    
-    (* use map.Map *)
-    
-    (* use frama_c_wp.memory.Memory *)
-    
     (* use Compound *)
     
     goal wp_goal :
-      forall t:int -> int, t1:addr -> int, a:addr, a1:addr, i:int.
+      forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int.
        let a2 = shiftfield_F1_FD_pos a1 in
-       let x = get t1 a2 in
+       let x = get t a2 in
+       let a3 = Load_S2_A a t in
+       let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
        not x = i ->
        region (base a1) <= 0 ->
        region (base a) <= 0 ->
-       linked t -> is_sint32 i -> is_sint32 x -> not invalid t a2 1 -> a2 = a
+       is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3
   end
-[wp] 2 goals generated
+[wp] 1 goal generated