Support for CVC5
The goal of this MR is to add CVC5 as a supported prover for Why3. The format of SMT models returned by CVC5 have changed, so we also have to update the parsing of SMT models.
Changes in SMT models are of the following form:
- (before, with CVC4)
(define-fun a () array @uc_array_0)
- (after, with CVC5)
(define-fun a () array (as @a0 array))