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.