[Why3-club] why3 execute: Cannot execute expression match

Guillaume Melquiond guillaume.melquiond at inria.fr
Fri Aug 19 14:48:19 CEST 2016


On 19/08/2016 11:20, David MENTRE wrote:
> Hello,
> 
> When trying to execute the attached WhyML file, I get following error:
> """
> $ why3 -C why3.config execute execute_test.mlw Execute_test.test
> Execution of Execute_test.test ():
>      type: bool
> 
> 
> Execution error: Cannot execute expression
>                  match ((cmd_previous,
>                  cmd_current)) with
>                  | False, True -> (True)
>                  | _, _ -> (False)
>                  end
> """
> 
> Is this a bug?

Yes. Boolean are hardcoded in the interpreter, but somehow the match
construct does not know about them.

> Should I open a bug on Why3 issue tracker?

Don't bother, it should be easy enough to fix (assuming my
interpretation is correct).

> Is there a work-around?

In the meantime, using your own boolean type rather than the standard
one should do the trick.

Best regards,

Guillaume


More information about the Why3-club mailing list