Performance difference when base address is fixed vs. symbolic in bitvector-based pointer analysis

[christophsanders]

I am using the Z3 solver for a static pointer analysis, where all variables are represented as bitvectors. I noticed a significant performance difference when my base allocation address is fixed (e.g., context.bv_val(10000, ...)) versus when it is a symbolic variable (e.g., context.bv_const(...)).

Here is a simplified example of what I am doing:

z3::expr base_adres_allocatie = context.bv_const(...);  // symbolic base
// z3::expr base_adres_allocatie = context.bv_val(10000, ...);  // fixed base (much faster)

z3::expr end_adres_allocatie = context.bv_const(...);
solver.add(end_adres_allocatie == base_adres_allocatie + ...);

z3::expr base_adres_memoryPointer = context.bv_const(...);
z3::expr end_adres_memoryPointer = context.bv_const(...);
solver.add(end_adres_memoryPointer == base_adres_memoryPointer + ...);

solver.add(base_adres_memoryPointer == base_adres_allocatie + ...);

// Check if the pointer goes out of bounds
solver.add(end_adres_memoryPointer > end_adres_allocatie);

if (solver.check() == z3::unsat) {
    // Allocation upper bound is safe
}

When base_adres_allocatie is a symbolic variable, the solver takes significantly longer to resolve the constraints. However, when I fix it to a specific value (bv_val), the solver is much faster.

Could someone explain why this happens? Are there optimizations in Z3 that benefit from fixed values in this kind of constraint setup? And are there any specific flags in z3 that optimise the solver to just find unsat scenarios because that's actually the only thing I'm interested in.

Thanks in advance!

[NikolajBjorner]

a lot of things are much easier when you use constant indices. They can be compared for equality directly without relying on anything structural. In other words we always know 2 != 5, but don't necessarily know up front that
x + 2 != x + 5 when processing formulas.

Is a base address really necessary for modeling? Can't a base address be baked into the arrays you use?