// Just a very simple example
S1(x:int , y:int | z:int){
  assume 1<x && x<y ;
  if x>10
     then { x := x - 1 ; y := x }
     else { y := x+1 } ;
  z := y ;
  assert z = x || z = x+1 // valid
  // assert x >= 10 && z = x+1 // not valid
}