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

David MENTRE dmentre at linux-france.org
Fri Aug 19 11:20:30 CEST 2016


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? Should I open a bug on Why3 issue tracker?

Is there a work-around?

I'm using Why3 0.87.0.

Best regards,
david
-------------- next part --------------
module Execute_test

 let f (cmd_previous cmd_current : bool) : bool
 = match cmd_previous, cmd_current with
   | False, True -> True
   | _, _ -> False
   end

 let test ()
 = f False True

end


More information about the Why3-club mailing list