CVC4 1.8 model Parsing error
With current master of cvc4, Why3 is unable to parse the model. The issue is cvc4 emitting declarations like this:
; cardinality of integer is 1 (declare-sort integer 0) (declare-fun () integer)
Why3 is unable to parse the last line. I will propose a (unelegant) patch which ignores such lines.