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
Hello,
I did not use CVC4 1.5 for enough time to compare with 1.4. Anyway,
I'd like to recommend:
1) to duplicate the prover entry, with an alternative name, instead of
modifying the existing one
2) to use the *-step options of CVC4 only for the "command_steps"
parameter, not the "command" one.
