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 would not give optimal results yet …” Now, why3-0.88.0 has been released. During configuration why3 suggests to upgrade from cvc4-1.4 : Found prover CVC4 version 1.4 (old version, please consider upgrading). I have evaluated therefore again version 1.5 of cvc4 against version 1.4. This time, however, version 1.5 could not prove any proof obligation from “ACSL by Example”! Again, I wonder, if there is anything on my side that we should have taken into account. Regards Jens
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
