#include<mem.cvh>

int main() {
  int x,y,z;

  x = 0, y = 0, z = 0;
  $read_set_push();
  int a = x + y;
  x = a;
  $mem m = $read_set_pop();
  $mem oracle = ($mem)&x;

  oracle = $mem_union(oracle, ($mem)&y);
  oracle = $mem_union(oracle, ($mem)&a);
  $assert($mem_equals(m, oracle));
}