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

Guillaume Melquiond guillaume.melquiond at inria.fr
Fri Aug 19 18:02:41 CEST 2016


On 19/08/2016 17:45, David MENTRE wrote:

>>>> Is there a work-around?
>> In the meantime, using your own boolean type rather than the standard
>> one should do the trick.
> 
> I failed to do it despite several attempts, see attached execute_test.mlw:

You just moved the matching issue from f to bool_t_of_bool. You should
have written the latter function as

 function bool_t_of_bool (b : bool) : bool_t
 = if b then DTrue else DFalse

so that it doesn't match on boolean values.

Best regards,

Guillaume


More information about the Why3-club mailing list