In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite fields. To support interoperability in this emerging ecosystem, we propose the SMT-LIB theory of finite field arithmetic (FFA). The theory defines a canonical representation of finite field elements as well as definitions of operations and predicates on finite field elements.

翻译：近年来，有限域的可满足性模理论求解取得了快速发展。这包括新的判定过程、有限域SMT理论求解器的新实现，以及依赖有限域SMT求解的新型软件验证工具。为支持这一新兴生态系统的互操作性，我们提出了有限域算术的SMT-LIB理论。该理论定义了有限域元素的规范表示，以及有限域元素上的运算和谓词的定义。