  This system description introduces an enhancement to the Yices2 SMT solver,
enabling it to reason over non-linear polynomial systems over finite fields.
Our reasoning approach fits into the model-constructing satisfiability (MCSat)
framework and is based on zero decomposition techniques, which find finite
basis explanations for theory conflicts over finite fields. As the MCSat solver
within Yices2 can support (and combine) several theories via theory plugins, we
implemented our reasoning approach as a new plugin for finite fields and
extended Yices2's frontend to parse finite field problems, making our
implementation the first MCSat-based reasoning engine for finite fields. We
present its evaluation on finite field benchmarks, comparing it against cvc5.
Additionally, our work leverages the modular architecture of the MCSat solver
in Yices2 to provide a foundation for the rapid implementation of further
reasoning techniques for this theory.
