liquid-fixpoint-8.10.7: tests/pos/len00-rename.fq

// This qualifier saves the day; solve constraints WITHOUT IT

qualif ListZ(v : [@(0)]): (len v >= 0)

constant len : (func(2, [(@(0)  @(1)); int]))

bind 0 y : {v : [(Tuple int a)] | [len v >= 0]}

constraint:
  env [0]
  lhs {v1 : [(Tuple int a)] | [v1 = y] }
  rhs {v1 : [(Tuple int a)] | [$k0[v0 := v1]]   }
  id 1 tag []

constraint:
  env []
  lhs {v2 : [(Tuple int a)] | [$k0[v0 := v2]]             }
  rhs {v2 : [(Tuple int a)] | [len v2 >= 0] }
  id 2 tag []

wf:
  env [ ]
  reft {v0 : [(Tuple int a)] | [$k0] }