Time complexity about pbeq and pble.

[TraceShadow]

I'm using z3 to construct some cnf and using some sat solvers to solve them. Now I have a expr_vector with N boolean variable. I want to express two constraints. One is exactly K out of N of them should be true and the other is at most K out of N should be true. I use pbeq to express the first constraint and use atmost to express the other one (the coefficient of all variable is always 1). Then I want to compare the time to solve these two constraints. It surprises me that atmost is always faster than pbeq (for unsat answer). I also try pble but get the same results. I wonder if this is the correct time comparison? Or did I do something wrong? If it is the truth, is there any other way to express these two constraints and satisfy the the time to solve the former constraint in less time than the latter?

[NikolajBjorner]

z3 doesn't has very superficial support for pbeq. It expands into a conjunction of pble and pbge.
Then pble is rewritten to pbge by negating variables and adjusting the bound using the sum of coefficients and subtract the old bound. So pbeq should never really be better. It could be that you are exposing an opportunity to build in direct handling of pbeq. For unsat answers may save some overhead with a single constraint. Z3 also has options for compiling PB constraints into CNF. These translations don't all have handling for equality so they use fallback methods if you pass in a pbeq.