Is z3 the most efficient solver for quantifier-fre

Question

Sorry that this question is subjective, but given that the Stack Overflow has the largest Z3 user base, I want to give it a try.

I have a big constraint satisfaction problem that consists of many integer propositional logic formulas and a few first order logic formulas that only contain integers(quantifiers). I care very much about the efficiency, because I am building an interactive program synthesizer.

I am now using z3 solver and the check time is sometimes too long. I wonder if z3 is the best tool to tackle the problem I mentioned in above or there is a better tool? How about CPLEX?

Any suggestion will be appreciated.

Edit:

Sorry, the code has been remove for privacy reason. I can email you my code personally if you are willing to take a look. Thanks in advance.