diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index c0af767bbf0912e5d74308d3d58028222dde7437..0eabe5d5f690a1566d86a63f1edaa6c318df9734 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -525,7 +525,8 @@ let pp_value pp fmt = function
 let pp_logic pp fmt = function
   | Vexp e -> F.pp_term fmt e
   | Vloc l -> pp fmt l
-  | Lset _ | Vset _ -> Format.pp_print_string fmt "<set>"
+  | Lset _ -> Format.pp_print_string fmt "<lset>"
+  | Vset vs -> Format.fprintf fmt "{ %a }" Vset.pretty vs
 
 let pp_rloc pp fmt = function
   | Rloc(obj,l) ->
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index bb695d8c004a37c4eb8aeeefe2d1f848dd7c240c..b49ce991d37a695a905a8bb2a2d3ee368d7548eb 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -320,7 +320,7 @@ struct
       let sa = set_of_term env a in
       let sb = set_of_term env b in
       (* TODO: should be parametric in the equality of elements *)
-      Vset.equal sa sb
+      Vset.equal ~use_eq:(use_equal polarity) sa sb
 
     | EQ_loc ->
       let la = loc_of_term env a in
@@ -686,7 +686,7 @@ struct
         | Ctype t -> Lang.assume (Cvalues.has_ctype t r)
         | _ -> ()
       end ;
-      Vexp r
+      Cvalues.plain t.term_type r
 
     | Tlambda _ ->
       Warning.error "Lambda-functions not yet implemented"
diff --git a/src/plugins/wp/Vset.ml b/src/plugins/wp/Vset.ml
index 1e54e5e5a665e3764ee184d72dafb3fb8337cc15..87bb24efac6a1936206c80b2395156d5529391ef 100644
--- a/src/plugins/wp/Vset.ml
+++ b/src/plugins/wp/Vset.ml
@@ -94,16 +94,31 @@ let pretty fmt = function
 let library = "vset"
 
 let adt_set = Lang.datatype ~library "set"
-let tau_of_set te = Logic.Data( adt_set , [te] )
-let p_member = Lang.extern_p ~library ~bool:"member_bool" ~prop:"member" ()
+let tau_of_set (te:tau) : tau = Logic.Data( adt_set , [te] )
+
+let typecheck_binop (params:tau option list) : tau =
+  match params with
+  | [ Some t ; _ ] | [ _ ; Some t ]-> t
+  | _ -> raise (Invalid_argument "WP.Vset.typecheck_binop")
+
+
+let typecheck_singleton (params:tau option list) : tau =
+  match params with
+  | [ Some t ] -> tau_of_set t
+  | _ -> raise (Invalid_argument "WP.Vset.typecheck_unop")
+
+let typecheck_range (_:tau option list) : tau =
+  tau_of_set Logic.Int
+
+let p_member = Lang.extern_p ~library ~bool:"memb" ~prop:"mem" ()
 let f_empty = Lang.extern_f ~library "empty"
-let f_union = Lang.extern_f ~library "union"
-let f_inter = Lang.extern_f ~library "inter"
-let f_range = Lang.extern_f ~library "range"
-let f_range_sup = Lang.extern_f ~library "range_sup"
-let f_range_inf = Lang.extern_f ~library "range_inf"
-let f_range_all = Lang.extern_f ~library "range_all"
-let f_singleton = Lang.extern_f ~library "singleton"
+let f_union = Lang.extern_f ~library ~typecheck:typecheck_binop "union"
+let f_inter = Lang.extern_f ~library ~typecheck:typecheck_binop "inter"
+let f_range = Lang.extern_f ~library ~typecheck:typecheck_range "range"
+let f_range_sup = Lang.extern_f ~library ~typecheck:typecheck_range "range_sup"
+let f_range_inf = Lang.extern_f ~library ~typecheck:typecheck_range "range_inf"
+let f_range_all = Lang.extern_f ~library ~typecheck:typecheck_range "range_all"
+let f_singleton = Lang.extern_f ~library ~typecheck:typecheck_singleton "singleton"
 
 let single a b = match a,b with
   | Some x , Some y when F.QED.equal x y -> a
@@ -237,8 +252,11 @@ let subset xs ys =
 (* --- Equality                                                           --- *)
 (* -------------------------------------------------------------------------- *)
 
-let equal xs ys =
-  p_and (subset xs ys) (subset ys xs)
+let equal ?(use_eq:bool=false) (xs:set) (ys:set) =
+  match xs, ys with
+  | [  Set (_,s1) ], [  Set (_,s2) ] when use_eq -> p_equal s1 s2
+  | _ -> p_and (subset xs ys) (subset ys xs)
+
 
 (* -------------------------------------------------------------------------- *)
 (* --- Separation                                                         --- *)
diff --git a/src/plugins/wp/Vset.mli b/src/plugins/wp/Vset.mli
index 6d5677b281cd4333dcff9b1d0e62816139fedfe0..9cd9a4820c2438913e60cc0d634cc9547900c806 100644
--- a/src/plugins/wp/Vset.mli
+++ b/src/plugins/wp/Vset.mli
@@ -51,7 +51,7 @@ val ordered : limit:bool -> strict:bool -> term option -> term option -> pred
     - [strict]: if [true], comparison is [<] instead of [<=] *)
 
 val is_empty : set -> pred
-val equal : set -> set -> pred
+val equal : ?use_eq:bool -> set -> set -> pred
 val subset : set -> set -> pred
 val disjoint : set -> set -> pred
 
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
index a2d895336550321e3e5101656b3d0a69fb7cd072..db63c2110a213c95139c7db30f8b169b3c522b58 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
@@ -21,80 +21,27 @@
 (**************************************************************************)
 
 (* -------------------------------------------------------------------------- *)
-(* --- Sets for Why-3                                                     --- *)
+(* --- Additional Sets Symbols for WP                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
 theory Vset
 
-  use bool.Bool
   use int.Int
+  use map.Const
+  use export set.Set
 
-  (* -------------------------------------------------------------------------- *)
-  (* --- Classical Sets for Alt-Ergo                                        --- *)
-  (* -------------------------------------------------------------------------- *)
-
-  type set 'a
-
-  function empty : set 'a
-  function singleton 'a : set 'a
-
-  function union (set 'a) (set 'a) : set 'a
-  clone algebra.AC as Lunion with type t = set 'a, function op = union with axiom .
-
-  function inter (set 'a) (set 'a) : set 'a
-  clone algebra.AC as Linter with type t = set 'a, function op = inter with axiom .
-
-  predicate member 'a (set 'a)
-  function member_bool 'a (set 'a) : bool
-
-  function range int int : set int (* [a..b] *)
-  function range_sup int : set int (* [a..] *)
-  function range_inf int : set int (* [..b] *)
-  function range_all : set int (* [..] *)
-
-  predicate eqset (a : set 'a) (b : set 'a) =
-    forall x : 'a. (member x a) <-> (member x b)
-
-  predicate subset (a : set 'a) (b : set 'a) =
-    forall x : 'a. (member x a) -> (member x b)
-
-  predicate disjoint (a : set 'a) (b : set 'a) =
-    forall x : 'a. (member x a) -> (member x b) -> false
-
-  (* -------------------------------------------------------------------------- *)
-
-  axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
-    if member x s then member_bool x s = True else member_bool x s = False
-
-  axiom member_empty : forall x:'a [member x empty].
-    not (member x empty)
-
-  axiom member_singleton : forall x:'a,y:'a [member x (singleton y)].
-    member x (singleton y) <-> x=y
-
-  axiom member_union : forall x:'a. forall a:set 'a,b:set 'a [member x (union a b)].
-    member x (union a b) <-> (member x a) \/ (member x b)
-
-  axiom member_inter : forall x:'a. forall a:set 'a,b:set 'a [member x (inter a b)].
-    member x (inter a b) <-> (member x a) /\ (member x b)
-
-  axiom union_empty : forall a:set 'a [(union a empty)|(union empty a)].
-    (union a empty) = a /\ (union empty a) = a
-
-  axiom inter_empty : forall a:set 'a [(inter a empty)|(inter empty a)].
-    (inter a empty) = empty /\ (inter empty a) = empty
+  function memb (x:'a) (s:set 'a) : bool = s x
 
-  axiom member_range : forall x:int,a:int,b:int [member x (range a b)].
-    member x (range a b) <-> (a <= x /\ x <= b)
+  let function range (inf sup:int) : set int (* [a..b] *) =
+    fun elt -> inf <= elt <= sup
 
-  axiom member_range_sup : forall x:int,a:int [member x (range_sup a)].
-    member x (range_sup a) <-> (a <= x)
+  function range_sup (sup:int) : set int (* [a..] *) =
+    fun elt -> elt <= sup
 
-  axiom member_range_inf : forall x:int,b:int [member x (range_inf b)].
-    member x (range_inf b) <-> (x <= b)
+  function range_inf (inf:int) : set int (* [..b] *) =
+    fun elt -> inf <= elt
 
-  axiom member_range_all : forall x:int [member x range_all].
-    member x range_all
+  function range_all : set int (* [..] *) = const true
 
   (* -------------------------------------------------------------------------- *)
 
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index ae31e0275d22732440e14447ede176473c954c36..2bbd925602a696a9392e6ad30bc658fe55cffb5d 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -81,7 +81,7 @@ logic sign "\\sign"(float64) = "sign_f64";
 
 library vset:
 type set = "set";
-why3.import := "vset.Vset";
+why3.import := "frama_c_wp.vset.Vset";
 
 library vlist:
 why3.import := "frama_c_wp.vlist.Vlist";
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..23b08c2fd1731435934b44c9a4e5bc188184661a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
@@ -0,0 +1,80 @@
+# frama-c -wp [...]
+[kernel] Parsing vset.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Check Lemma 'direct_in':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check Lemma 'direct_in_singleton':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_equal_constants':
+Prove: mem(1, L_Set1) /\ mem(2, L_Set1) /\ mem(3, L_Set1) /\
+    (forall i : Z. (mem(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_equal_ghost':
+Let a = L_Set2(int2_0, int1_0).
+Assume { Have: is_sint32(int1_0). Have: is_sint32(int2_0). }
+Prove: mem(int1_0, a) /\ mem(int2_0, a) /\
+    (forall i : Z. (mem(i, a) -> ((i = int1_0) \/ (i = int2_0)))).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_equal_logical':
+Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\
+    (forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2)))).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_in_constants':
+Prove: mem(2, L_Set1).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_in_ghost':
+Assume { Have: is_sint32(int2_0). }
+Prove: mem(int2_0, L_Set2(int2_0, int1_0)).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_in_logical':
+Prove: mem(2, L_Set3).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_not_equal_constants':
+Prove: (!mem(0, L_Set1)) \/ (!mem(1, L_Set1)) \/ (!mem(2, L_Set1)) \/
+    (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set1)).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_not_equal_logical':
+Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/
+    (exists i : Z. (i != 0) /\ (i != 1) /\ mem(i, L_Set3)).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_not_in_constants':
+Prove: !mem(4, L_Set1).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'indirect_not_in_logical':
+Prove: !mem(0, L_Set3).
+
+------------------------------------------------------------
+
+Goal Check Lemma 'test':
+Assume { Have: (b = a) \/ (c = b). Have: mem(i, b). }
+Prove: mem(i, a) \/ mem(i, c).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1d2ca2989c338ac98fbbdb6d38bf85c35a742b9d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
@@ -0,0 +1,24 @@
+# frama-c -wp [...]
+[kernel] Parsing vset.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 13 goals scheduled
+[wp] [Valid] typed_check_lemma_direct_in (Qed)
+[wp] [Valid] typed_check_lemma_direct_in_singleton (Qed)
+[wp] [Valid] typed_check_lemma_indirect_equal_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_equal_ghost (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_equal_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_ghost (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_equal_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_equal_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_in_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_test (Alt-Ergo) (Cached)
+[wp] Proved goals:   13 / 13
+  Qed:             2
+  Alt-Ergo:       11
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     2       11       13       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/vset.i b/src/plugins/wp/tests/wp_acsl/vset.i
new file mode 100644
index 0000000000000000000000000000000000000000..922c058e325fad0a38d35c88914cec9ff8cc6083
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/vset.i
@@ -0,0 +1,30 @@
+
+//@ check lemma direct_in: 2 \in {1,2,3};
+//@ check lemma direct_in_singleton: 2 \in {2};
+
+//@ logic set<integer> Set1 = {1,2,3};
+//@ check lemma indirect_in_constants: 2 \in Set1;
+//@ check lemma indirect_not_in_constants: ! (4 \in Set1);
+//@ check lemma indirect_equal_constants: Set1 == {1,2,3};
+//@ check lemma indirect_not_equal_constants: Set1 != {0,1,2};
+
+//@ logic integer i0 = 0;
+//@ logic integer i1 = 1;
+//@ logic integer i2 = 2;
+//@ logic set<integer> Set3 = {i1,i2};
+//@ check lemma indirect_in_logical: i2 \in Set3;
+//@ check lemma indirect_not_in_logical: ! (i0 \in Set3);
+//@ check lemma indirect_equal_logical: Set3 == {i1,i2};
+//@ check lemma indirect_not_equal_logical: Set3 != {i0,i1};
+
+//@ ghost int int1 = 1;
+//@ ghost int int2 = 2;
+//@ logic set<int> Set2 = {int1,int2};
+//@ check lemma indirect_in_ghost: int2 \in Set2;
+//@ check lemma indirect_equal_ghost: Set2 == {int1,int2};
+
+/*@ check lemma test:
+  @   \forall set<int> a,b,c;
+  @   (a == b || b == c) ==>
+  @   (\union(a,\union(b,c)) == \union(a,c));
+  @*/