Vale/Dafny does not generate invocation to the callee procedure if callee is defined after the caller function

[superymk]

Tested with Vale-0.3.10.

Code:

procedure caller(
    out result:reg
)
    reads
        eax;
    modifies
        ebx; ecx;
{
    callee(eax, ebx);

    MOV(ecx, ebx);
}

procedure callee(
    in bool1:reg,
    out result:reg
)
    reads
        eax;
{
    MOV(result, 1);
}

Expect:

function method{:opaque} va_code_caller(result:va_operand_reg):va_code
{
  va_Block(va_CCons(va_code_callee(va_op_reg_reg(EAX), va_op_reg_reg(EBX)),
    va_CCons(va_code_MOV(va_op_word_reg(ECX), va_op_word_reg(EBX)), va_CNil())))
}

Current:

function method{:opaque} va_code_caller(result:va_operand_reg):va_code
{
  va_Block(va_CCons(va_code_MOV(va_op_word_reg(ECX), va_op_word_reg(EBX)), va_CNil()))
}