Non-short-circuiting operators are short-circuiting

[superaxander]

In Java the following program verifies where it shouldn't:

class Test {
    int a;

    //@ context Perm(a, write);
    //@ ensures a == \old(a) + 1;
    //@ ensures !\result;
    boolean inc() {
        a += 1;
        return false;
    }

    //@ context Perm(a, write);
    //@ requires a == 0;
    void foo() {
        boolean b = inc() & inc();
        //@ assert !b;
        // Should fail because & is not short-circuiting (i.e. a should be 2
        //@ assert a == 1;
    }
}

In the Disambiguate rewrite pass bitwise operations on booleans are simply replaced with the short-circuiting operator variants. (The other front ends either don't parse the bitwise operators at all or keep them until the end crashing VerCors)