(* example

  int x,y; 
  //@ requires x == 0
  //@ ensures  x == 1
  void main() { y=0; x=1; assert {y==0} }

  logic x : int
  logic y : int
  axiom sep_x_y : x <> y

  forall m1:memory.
  forall m2:memory. m2=upd(m1,y,0) -> 
  forall m3:memory. m3=upd(m2,x,1) -> 
  acc(m3,y)=0

*)