Scribble miscompiles lets inside of an implication

[cd1m0]

Given the annotation: /// #if_succeeds cond ==> let x := E0 in E1; scribble will produce the following instrumentation:

    let x_0 := E0;
    if ((!cond) || E1) {
        ...
    }

This is incorrect, since E0 will always be evaluated, even when cond is false. This is can cause unexpected crashes. Fix it.