BinarySearch.dfy(44,19): Error: result of operation might violate newtype constraint
Execution trace:
    (0,0): anon0
    BinarySearch.dfy(40,3): anon18_LoopHead
    (0,0): anon18_LoopBody
    BinarySearch.dfy(40,3): anon19_Else
    BinarySearch.dfy(40,3): anon23_Else

Dafny program verifier finished with 6 verified, 1 error