why3 execute type inference problem
I came across a surprising behavior of the why3 execute
command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue () =
let l = inorder Empty in
assert { l = Nil }
end
With why3 ide
, it behaves as excepted : one VC is generated, and the assertion is easily discharged automatically.
With why3 execute
, I get the following error message :
$ why3 execute issue.mlw --use=Issue 'issue ()'
Type mismatch between bintree.Tree.tree 'a and bintree.Tree.tree 'xi
Is this a known issue for version 1.6.0 of why3 ?
I have tried to provide more guidance to type inference using type annotations, but this doesn't solve the problem.
Thanks