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.