Hello again,
Le 13/05/2021 à 18:09, David MENTRÉ a écrit :
I have a strange issue with Why3 1.3.3: it does not detect alt-ergo in
the PATH.
I do have alt-ergo installed and running:
david:~$ which alt-ergo
~/.opam/4.11.1/bin/alt-ergo
david:~$ alt-ergo --version
2.4.0
However it does not detect alt-ergo while it correctly finds other
provers:
david:~$ why3 config --detect-provers
Found prover CVC4 version 1.3 (old version, please consider upgrading).
Found prover CVC3 version 2.4.1, OK.
Found prover Vampire version 0.6, OK.
Found prover Z3 version 4.3.1 (old version, please consider upgrading).
Found prover Z3 version 3.2 (old version, please consider upgrading).
Found prover Zenon version 0.7.1, OK.
6 prover(s) added
Save config to /home/david/.why3.conf
OK, I found it using --debug option:
<0.005760,autodetect>Run: (alt-ergo -version) > /tmp/outddaf02 2>&1
<0.014554,autodetect>command 'alt-ergo -version' failed. Output:
alt-ergo: unknown option `-e', did you mean `--version' ?
Usage: alt-ergo [OPTION]... [FILE]
Try `alt-ergo --help' for more information.
alt-ergo 2.4.0 has changed command line options, for more usual GNU-like
options.
I downgraded to Alt-Ergo 2.3.3 which, while said unsupported by Why3,
seems to work fine.
Best regards,
david
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
