Is z3 the most efficient solver for integer sentence logic without a quantifier?

Question

Sorry this question is subjective, but given that Qaru has the largest Z3 user base, I want to try.

I have a problem with a large restriction of restrictions, consisting of many integer logical formulas of the sentence and several logical formulas of the first order, which contain only integers (quantifiers). I care a lot about efficiency because I create an interactive software synthesizer.

Now I am using the z3 solver, and the verification time is sometimes too long. I wonder if z3 is the best tool to solve the problem that I mentioned above, or is there a better tool? What about CPLEX?

Any suggestion would be appreciated.

Edit:

Sorry, the code has been removed for privacy reasons. I can send you my code personally if you want to take a look. Thanks in advance.