I understand that in general, non-linear integer arithmetic is undecidable. However, this is not the case for the arithmetic of finite fields mod p, as in particular this can be reduced to a SAT problem over finite bit vectors. The reduction to SAT is however, it seems, somewhat inefficient for large primes p (this is Z3's default behaviour).

Is there a more efficient way of modelling arithmetic operations in Z3 over such a finite field? Perhaps performance improvements can be made over Z3's default strategy from the knowledge that all arithmetic operations are over the same finite field?