[Why3-club] simple propositional logic in why3 (with alt-ergo)
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
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