Hi Why3 Club
Le 10/05/2019 à 08:30, Guillaume Melquiond a écrit :
I would expect Why3 to use
Please note that such a sentence is meaningless: Why3 is not a prover
per se, it calls external provers. If you ask
"I would expect Alt-Ergo/CVC4/Z3 to use ..."
then see Guillaume answer.
An alternative is to additionally use non-SMT-based provers, such as the
E prover or Spass, which prove your goal as you expect.
- Claude
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
