module main {
    var x : integer;

    init {
        x = 3;
    }

    procedure ActionA()
    modifies x;
    {
        x = 2 * x;
    }

    procedure ActionB()
    modifies x;
    {
        x = x + 1;
    }

    next {
        if (*) {
            call ActionA();
        } else {
            call ActionB();
        }
    }

    control {
        v = unroll(5);
        check;
        print_results;
    }
}
