Invalid coma output ("unbound function or predicate symbol (+)")

[Armael]

The following example generates invalid coma code:

use creusot_contracts::*;

pub enum Q {
    Zero,
    Frac1(Int),
}
use Q::*;

impl Invariant for Q {
    #[predicate]
    #[open]
    fn invariant(self) -> bool { true }
}

impl Q {
    #[logic]
    #[ensures(result.invariant())]
    fn mul(self, y: Q) -> Q {
        match (self, y) {
            (Zero, _) => Zero,
            (_, Zero) => Zero,
            (Frac1(n), Frac1(m)) => Frac1(n + m),
        }
    }
}

.coma output (extract). The error is on the line with n + m:

...
  goal vc_mul : match (self, y) with
    | (Q'0.C_Zero, _) -> [%#stest0] invariant'0 (Q'0.C_Zero)
    | (_, Q'0.C_Zero) -> [%#stest0] invariant'0 (Q'0.C_Zero)
    | (Q'0.C_Frac1 n, Q'0.C_Frac1 m) -> [%#stest0] invariant'0 (Q'0.C_Frac1 (n + m))
    end
...