If Then Else expressions do not carry guard information into body

[Daniel-Cumming]

I might of found a small bug in Vale. I'm not sure if this is intentional, but when using an if then else expression the information from the guard isn't passed to the scope of then or else branches. This means that an error might be thrown in the branch that you have excluded in the guard. I wrote an minimum example to show what I mean (I added the procedure to the end of Test.MemCpy.vaf).

procedure IfThenElseError() 
    reads 
        rax;
        rbx;
    modifies
        rcx;    
    ensures 
        rcx == (if rbx = 0 then 0 else rax % rbx); // This is line 154
{}

Error Message:
error at line 154 column 44 of file ./fstar/code/test/Test.Memcpy.vaf:
cannot find new bound for '(Int 0, Int 18446744073709551615) BMod (Int 0, Int 18446744073709551615)'
scons: *** [obj/fstar/code/test/Test.Memcpy.fst] Error 1
scons: building terminated because of errors.

The error can be avoided by casting rbx to be non-zero (however this information is already available from the guard):

procedure IfThenElse() 
    reads 
        rax;
        rbx;
    modifies
        rcx;    
    ensures 
        rcx == (if rbx = 0 then 0 else rax % #pos(rbx));
{}

Above produces a verification error as expected since the procedure as no implementation to guarantee the spec.