Hello,
As far as I understand, the problem is more about putting data with
invariant inside a compound type like a list.
I suggest you proceed without using the invariant feature but do it "by
hand" such as
type lit = { var : int ; sign : bool }
predicate wf_lit (l:lit) = l.var >= 0
let
Hi,
It seems to me that Why3 considers any record type with an invariant as
immutable. Indeed,
the following code gets me an error:
```
type lit = { var : int ; sign : bool } invariant { self.var >= 0 }
let f (ls : list lit) =
requires { forall l:lit. mem l ls } ()
```
Error: Cannot u
