Hello,
in „ACSL by Example“ (https://fraunhoferfokus.github.io/acsl-by-example/), we
have been using the
prover CVC4 through Why3 for quite some time.
Recently, a new version (1.5) of CVC4 was released.
Unfortunately, it appears that this new version can discharge considerably
fewer of our proo
Hello,
I have seen the announcement for why3-0.88.0 but it is not yet available
through opam.
Is there a particular reason for this?
Regards
Jens
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/list
oming
> really strict and check a lot of situations and cases before a
> new package is accepted.
>
> Why3 0.88.0 has been proposed 7 days ago, but it's still not
> included in the repo:
>
> https://github.com/ocaml/opam-repository/pull/10413
>
With a clean install of opam I had no problems to install why3-0.88.0.
By the way, when calling ‘why3 config –detect’ I receive now the message
Prover Eprover (2.0) will be used in Auto level >= 2
Prover Alt-Ergo (1.30) will be used in Auto level >= 1
Prover CVC4 (1.5) will be used in Auto
Hello,
A while ago I experimented with why3-0.87.3 and cvc4.
At that time I reported that version 1.5 of cvc4 performed considerable worse
than version 1.4.
This issue was later explained that cvc4_15.drv
“… was made before the actual release of cvc4 1.5. Even cvc4_15.drv from Why3
master woul
Hello,
I am using why3 0.88.3 without problems on my Mac(s).
I remember that there was an issue with ocaml which made it necessary to resort
to ocaml version 4.05.0.
Which version of ocaml are you using?
Regards
Jens
___
Why3-club mailing list
Why3-c
