qualif Cmp(v:a): (v = 10)
qualif Cmp(v:a): (v = 12)

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

constraint:
  env []
  lhs {v : int | [$k_0]}
  rhs {v : int | [v != 10]}
  id 4 tag [4]

constraint:
  env []
  lhs {v : int | [v = 12]}
  rhs {v : int | [$k_0]}
  id 2 tag [5]

constraint:
  env []
  lhs {v : int | [$k_0]}
  rhs {v : int | [v != 12]}
  id 3 tag [6]

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