liquid-fixpoint-0.8.0.2: tests/neg/ebind-01.fq
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 = 20 + m }
id 2 tag []