bad-subst01.fq

// fixpoint "--eliminate=some"


qualif Zog(v:a)  { 10 <= v }
qualif Bog(v:a, x:a)  { x <= v }

bind 0 a : {v: int | $k0 }

// this is a junk binder that adds a bogus [param := zogbert] substitution
// at each USE of k0 causing eliminate to crash.

bind 10 zogbert : {v : int | [] }

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

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

constraint:
  env [ 0 ]
  lhs {v : int | v = a}
  rhs {v : int | 10 <= v}
  id 3 tag []

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