[Why3-club] "if formula then" in expressions?

Guillaume Melquiond guillaume.melquiond at inria.fr
Wed Nov 7 09:07:20 CET 2012

Le mercredi 07 novembre 2012 à 08:49 +0100, Alan Schmitt a écrit :
> Hello,
> Why3 accepts program expressions of the form "if formula then ...". This
> does not seem to make sense as such a program could not be executed. Is
> this a bug or am I missing something?

This is not a bug. Possibly, the thing you are missing is that "x < y"
is a formula. (Sure, decidable formulas are just a tiny part of all the
formulas, so I understand how troubling such if-then-else expressions
might be.)

Best regards,


More information about the Why3-club mailing list