diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index e1ae3720d5110f20b5fae379864311994aad9221..aac2295277c1a6dd9d9d60176dfe5a7d57192afe 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -681,7 +681,12 @@ struct
         | ACSLDEF -> C.call_fun env result f ls vs
         | HACK phi -> phi vs
         | LFUN f -> e_fun ~result f vs
-      in Vexp r
+      in
+      begin match t.term_type with
+        | Ctype t -> Lang.assume (Cvalues.has_ctype t r)
+        | _ -> ()
+      end ;
+      Vexp r
 
     | Tlambda _ ->
       Warning.error "Lambda-functions not yet implemented"
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
index 37f7d58dc5b77e30a227642cd99a093b0401f84a..d2766c72bfc0fcdca2fa12d401ecf0cf8f2a9452 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
@@ -24,7 +24,13 @@ Prove: (0 <= L_t) /\ (L_t <= 127).
 ------------------------------------------------------------
 
 Goal Post-condition 'A' in 'g':
-Assume { (* Heap *) Type: region(p.base) <= 0. }
-Prove: L_x(Mint_0, p) <= 255.
+Let x = Mint_0[p].
+Let x_1 = L_x(Mint_0, p).
+Assume {
+  Type: is_uint8(x) /\ is_uint8(x_1).
+  (* Heap *)
+  Type: region(p.base) <= 0.
+}
+Prove: (x = x_1) /\ (x_1 <= 255).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
index 4dd7571870e8792ccb83e5393c72d9938a506a54..1ab51dfc81143d34f4c59499f6223fda24b53540 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
@@ -43,15 +43,20 @@ end
     
     (* use frama_c_wp.memaddr.MemAddr *)
     
+    (* use frama_c_wp.cint.Cint *)
+    
     (* use Axiomatic1 *)
     
     goal wp_goal :
-      forall t:addr -> int, a:addr. region (a.base) <= 0 -> L_x t a <= 255
+      forall t:addr -> int, a:addr.
+       let x = get t a in
+       let x1 = L_x t a in
+       region (a.base) <= 0 -> is_uint8 x -> is_uint8 x1 -> x = x1 /\ x1 <= 255
   end
-[wp] [Unsuccess] typed_g_ensures_A (Alt-Ergo) (Cached)
-[wp] Proved goals:    0 / 1
-  Unsuccess:       1
+[wp] [Valid] typed_g_ensures_A (Alt-Ergo) (Cached)
+[wp] Proved goals:    1 / 1
+  Alt-Ergo:        1
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  g                         -        -        1       0.0%
+  g                         -        1        1       100%
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i b/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i
index 6dd01e0b069cd98d104cf26c0334c19fac0b201b..32606dca6f36bcaf8686a1a6397845ca4e948f82 100644
--- a/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i
+++ b/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i
@@ -16,5 +16,5 @@
   @ ensures qed_ko: 0<=t<128 ; */
 void f(void) {return;}
 
-//@ ensures A: x(p) <= 255 ;
+//@ ensures A: *p == x(p) <= 255 ;
 void g(unsigned char* p){}