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.

翻译：本系统描述介绍了对Yices2 SMT求解器的一项增强，使其能够对有限域上的非线性多项式系统进行推理。我们的推理方法契合了模型构造可满足性（MCSat）框架，并基于零分解技术，该技术可为有限域上的理论冲突寻找有限基解释。由于Yices2内部的MCSat求解器可通过理论插件支持（并组合）多种理论，我们将推理方法实现为有限域的新插件，并扩展了Yices2的前端以解析有限域问题，从而使我们的实现成为首个基于MCSat的有限域推理引擎。我们在有限域基准测试上评估了该实现，并将其与cvc5进行了比较。此外，我们的工作利用了Yices2中MCSat求解器的模块化架构，为快速实现该理论的进一步推理技术奠定了基础。