Type mismatch when cloning
If I have the following code:
module A
exception E
let f (b: bool): int
raises { E }
=
(if b then return 0);
raise E
end
module B
clone A
end
Then I get the following error when I try to prove it:
$ why3 prove -P z3 bug.mlw
File "bug.mlw", line 12, characters 8-9:
warning: cloned theory .A does not contain any abstract symbol; it should be used instead
File "bug.mlw", line 12, characters 2-9:
Type mismatch between int and ()
However, if I comment out the "clone A" line, I don't get the "type mismatch" error anymore.
Is this expected?
If so, how am I supposed to fix f
to avoid this error when cloning?
Thanks in advance.