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求解器的模块化架构，为该理论领域内其他推理技术的快速实现奠定了基础。