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

Johannes Kanig kanig at adacore.com
Wed Sep 19 15:28:38 CEST 2012

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?


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list