liquid-fixpoint-0.6.0.1: tests/neg/poly2.fq

fixpoint "--defunct"

// This definition works fine ...
// constant offset : (func(0, [int ; int ; (BitVec Size32) ]))

// But this crashes as 'offset 0' is embedded as int not bv...
constant offset : (func(2, [@(0); int; int; @(0); @(1)]))

bind 0 x  : {VV : (BitVec  Size32) | [ VV = offset 0 0 0 0 ]}

constraint:
  env [0]
  lhs {VV : (BitVec Size32) | [ VV = x ] }
  rhs {VV : (BitVec Size32) | [ VV != x ] }
  id 1 tag [1]