fixpoint "--eliminate=all"

bind  1 m  : {v: int | true }
ebind 2 x1 : { int }
// bind  2 x1 : {v: int | v = m + 1 }

constraint:
  env [1; 2]
  lhs {v : int | v = m + 1 }
  rhs {v : int | v = x1    }
  id 1 tag []

constraint:
  env [1; 2]
  lhs {v : int | v = x1 + 1}
  rhs {v : int | v = 2 + m }
  id 2 tag []