[Why3-club] why3 execute: Cannot execute expression match
guillaume.melquiond at inria.fr
Fri Aug 19 14:48:19 CEST 2016
On 19/08/2016 11:20, David MENTRE wrote:
> 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)
> 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.
More information about the Why3-club