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

Alan Schmitt alan.schmitt at polytechnique.org
Wed Sep 19 15:43:10 CEST 2012


Johannes Kanig <kanig at adacore.com> writes:

> On 09/19/2012 03:17 PM, Alan Schmitt wrote:
>> Is it a problem with alt-ergo, with why3, or (more probably) with what I
>> wrote?
>
> It works on my system, but I have very recent why3 and alt-ergo
> versions. Still, the example is so simple that it looks like a setup issue.
>
> How do you run Alt-ergo? Do you use why3ide?
>
> You could output the Alt-Ergo VC to a file (using option -o of why3) and
> run Alt-Ergo by hand, what does it say?

I found out the issue: it was a path problem. Somehow why3ide was
launched in a way it could not find alt-ergo's binary. Sorry for the
noise.

Alan



More information about the Why3-club mailing list