Mentions légales du service

Skip to content

Support for CVC5

MOREAU Solene requested to merge cvc5 into master

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))
Edited by MOREAU Solene

Merge request reports