z3inc vs z3bitvectorinc for TCG

[sohah]

I am observing behavior difference when running z3inc and z3bitvectorinc on the following code:

public int testERInline(boolean a, int x) {
        int z = 0;
        if (a)
            z = testingER1(a, x);
        return z;
    }

    private int testingER1(boolean a, int x) {
        int z = 1;
        if (x > 2) {
            return z;
        }

        this.sideEffect = 5;

        z++;

        return z;
    }

Running the above with

listener =.symbc.BranchListener,gov.nasa.jpf.symbc.sequences.ThreadSymbolicSequenceListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener
coverageMode=3

with the z3incvector turned on, throws an exception due to the non-existence of an object in the solver query. The same behavior is not noticed when using z3inc. I need to understand the difference in behavior and tune TCG for the bitvector mode.