qualif Nat(v:int) : (0 <= v)

bind 0 x : {v: int | [$k0]}
bind 1 y : {v: int | [$k0]}
bind 2 z : {v: int | [$k1]}

constraint:
  env [ ]
  lhs {v : int | [v = 10]}
  rhs {v : int | [$k0]}
  id 1 tag [0]

constraint:
  env [ 0 ]
  lhs {v : int | [v = x + x]}
  rhs {v : int | [$k0]}
  id 2 tag [0]

constraint:
  env [ 0; 1 ]
  lhs {v : int | [v = x + y ]}
  rhs {v : int | [$k1]}
  id 3 tag [0]


constraint:
  env [ 2 ]
  lhs {v : int | [v =  z]}
  rhs {v : int | [0 <= v]}
  id 4 tag [0]

wf:
  env [ ]
  reft {v: int | [$k0]}


wf:
  env [ ]
  reft {v: int | [$k1]}