If instead of integers, our programs manipulate sets, the verification conditions will be in the set language and we can decide them by translation into exists-forall class.

Example: showing that a program that takes elements from set A and sorts into sets B and C, never loses any elements.

 A = A0;
 B = {};
 C = {};
 while //: inv "..."
   (A != {}) {
   pick x in A;
   if (condition(x)) {
     B = B union {x};
   } else {
     C = C union {x};
   }
 }
 assert(B union C = A0);