Performance difference between solvers

[rafaelsamenezes]

At ESBMC we noticed a benchmark with a huge difference between exporting SMT2 from Boolector and Z3 (esbmc/esbmc#1698). Specifically, Boolector took 5s and I could not reach a solution with Z3 under 5min. Also, extracting the boolector formula and feeding it to Z3 gave the same performance (<5s).

Could you please advise whether there is a configuration to make Z3 have a similar performance?
z3-flat.txt
btor-formula.txt

[NikolajBjorner]

no configuration at the moment.
It is all pre-processing.
You have a huge set of stores into something that has no effect.
Boolector implements pre-processing that Z3 does not have at the moment.

It may be as simple as detecting that

   F[(store A I E)] is equi-satisfiable to F[A]  

where F is a formula context, A an array, I an index, and E an element.

For your formula I are all constant indices, E are disjoint extracts into a bit-vector that isn't used elsewhere.
Thus, E are essentially non-aliased nonces. E is therefore unconstrained. A is also unconstrained.
This would allow the simplification.

[rafaelsamenezes]

Thanks for the feedback,

I will implement this pre-processing at ESBMC level then and check if it gives us the same performance boost then.

[NikolajBjorner]

ehm, this was not as complicated. Z3 has an inefficiency when handling large stores with constant offsets.
I added a throttle to avoid this.
The rewrite is direct because at the top level you use a select with a constant address into an array of constant addresses.
It now takes a few seconds to complete.

[lucasccordeiro]

Many thanks, @NikolajBjorner.