[Why3-club] simple propositional logic in why3 (with alt-ergo)

Virgile Prevosto virgile.prevosto at m4x.org
Wed Sep 19 15:37:59 CEST 2012


Hello Allan,

2012/9/19 Alan Schmitt <alan.schmitt at polytechnique.org>:
>
> HighFailure (0.10s)
> Prover exit status: exited with status 127
> Prover output:
>

in POSIX, exit status 127 means that the command that was expected to
be launched has not been found. Thus, I agree with Johannes, it looks
like a setup issue.
What does "why3config --detect-provers¨  say about alt-ergo?

-- 
E tutto per oggi, a la prossima volta
Virgile



More information about the Why3-club mailing list