Guided-none did not hit all branches

[S1eGa]

From sv-benchmarks; run on ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.i with guided-error=none and symbolic sizes hit only 50% of branches. But KLEE original and KLEE-utbot with guided mode hit all.

int main() {
    int* x = __builtin_alloca (sizeof(int));
    int* y = __builtin_alloca (sizeof(int));
    int* z = __builtin_alloca (sizeof(int));
    *x = __VERIFIER_nondet_int();
    *y = __VERIFIER_nondet_int();
    *z = __VERIFIER_nondet_int();
    while (*x > 0) {
        *x = *x + *y;
        *y = *z;
        *z = -(*z) - 1;
    }
}

[S1eGa]

Same problem on Urban-alloca.i