Surprising warnings about unused variables

[fpottier]

Is this valid Gospel?

let foo () =
  (0, 1)
(*@ (a, b) = foo()
    ensures a = 0
    ensures b = 1 *)

When I feed this into Cameleer, I get these warnings:

File "/Users/fpottier/dev/inferno/src/Bar.ml", line 3, characters 5-6:
warning: unused variable b
File "/Users/fpottier/dev/inferno/src/Bar.ml", line 3, characters 2-3:
warning: unused variable a

Yet, verification (with Z3) succeeds. The warnings are surprising because the variables a and b are actually used in the two ensures clauses. Furthermore, the locations of the warnings are incorrect (the line number seems correct but the column numbers are off).