diff --git a/tests/spec/tsets.c b/tests/spec/tsets.c
index 7adc987db2fda9ce46e75744dcb02ef63322e1c1..61d8e7f4689663c7dad8ba27ca51077e7bb816e0 100644
--- a/tests/spec/tsets.c
+++ b/tests/spec/tsets.c
@@ -68,3 +68,6 @@ int *AA(void);
 //@ logic set<integer> Sadd_elem_1(set<integer> s, integer e) = \union(s,e) ;
 //@ logic set<integer> Sadd_elem_2(set<integer> s, integer e) = \union(s,{e}) ;
 
+//@ predicate Smember_and(set<integer> s, integer v1, integer v2) = v1 & v2 \in s ;
+//@ predicate Smember_or (set<integer> s, integer v1, integer v2) = v1 | v2 \in s ;
+