Why does the latest version of Z3 solve slower than version 4.8.5?

[FangStars]

Recently I have been working on a project using version 4.8.5 of Z3, and I was hoping to improve efficiency by replacing it with the latest version of Z3 solver (4.12.2). However, after replacement, I was surprised that the efficiency decreased by half instead of increasing.

The statistics of both versions are shown below. I found that the number of "added-eqs" is exceptionally high in Z3-4.12.2; maybe this is the possible cause? Since I have not found an interpretation of the statistics, I need help understanding the reason behind this observation.

statistics of Z3-4.8.5

solve time 19124ms (:added-eqs 1796 :arith-add-rows 1641128 :arith-assert-diseq 773 :arith-assert-lower 493858 :arith-assert-upper 594258 :arith-bound-prop 66366 :arith-conflicts 1865 :arith-eq-adapter 70 :arith-pivots 54515 :binary-propagations 5994024 :conflicts 7045 :decisions 49053 :del-clause 47507 :eliminated-vars 2143 :max-memory 144.27 :memory 65.83 :minimized-lits 30346 :mk-bool-var 60936 :mk-clause 126002 :num-allocs 11964118888.00 :num-checks 1 :propagations 8269795 :restarts 52 :rlimit-count 196206713)

statistics of Z3-4.12.2

solve time: 40823ms (:added-eqs 736667 :arith-bound-propagations-lp 80406 :arith-conflicts 2028 :arith-fixed-eqs 136722 :arith-lower 901948 :arith-make-feasible 46745 :arith-max-columns 6641 :arith-max-rows 3591 :arith-offset-eqs 669474 :arith-upper 1402825 :binary-propagations 5521195 :conflicts 6815 :decisions 36939 :del-clause 31938 :max-memory 191.56 :memory 98.87 :minimized-lits 29012 :mk-bool-var 57001 :mk-clause 120518 :mk-clause-binary 66047 :num-allocs 34165268657.00 :num-checks 1 :propagations 7992977 :restarts 8 :rlimit-count 30604716 :solve-eqs-elim-vars 1971 :solve-eqs-steps 5823 :time 40.82)

The project code is written in Java language, and tactics "simplify," "propagate-values," "solve-eqs," "bit-blast," and "smt" are used in order when creating a solver with function mkSolver(). I also have tried to create the solver without any tactics. However, the solving time of Z3-4.12.2 is still longer than Z3-4.8.5 (52 s vs 31 s).

I am surprised by this observation, and I want to understand the reasons behind it.

Thanks!

[NikolajBjorner]

1. for reproducibility you could save the benchmark to an SMT2 file using the toString() method on the solver object.
2. You could set the parameter "smt.arith.solver" to 2 to enable the old solver. Since 4.8.5 there is a new arithmetic core. It turns out to very often be noticeable slower on applications.
3. A fluctuation by 2x is not uncommon even with the same solver, but for different random seeds. You could try a few different random seeds to check if behavior is consistently worse (with the new solver).

We would like to fix performance regressions in the new solver, even though it is non-trivial. Learning from user benchmarks is one approach.

[FangStars]

Thanks very much for your advice!

1. I saved the SMT2 file using the toString() method and found that different versions generate different files, though they look the same. The two SMT2 files are attached below. z3-4.8.5-SMT2.txt z3-4.12.2-SMT2.txt
2. I set the parameter "smt.arith.solver" to 2 under the z3-4.12.2, and it turns out that the solving efficiency speed up 2x compared to no parameter setting (68s vs 33s). The result is the same as the observation mentioned above.
3. Forgive me for not understanding the meaning of random seeds in Z3. I haven't done this experiment yet.

According to the experiment result, it seems like the efficiency reduction is caused by the arithmetic core. Since I am not familiar with the arithmetic-solving process, can you please indicate the reason behind it?

Thanks!

[NikolajBjorner]

Thanks, at this point use smt.solver=2 for your application. We will use your file to tune the new arithmetic solver.