packages feed

liquid-fixpoint-0.7.0.3: tests/cut/test00-tx.fq


// This qualifier saves the day; solve constraints WITHOUT IT
// qualif Zog(v:a) : (10 <= v)

bind 0 a : {v:int | (v = 10 || v = 20) }

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