夜雨聆风近日，2026年度国际SMT求解器竞赛（SMT-COMP 2026）公布结果。中国科学院软件研究所基础软件与系统重点实验室基础软件测试与分析研究室研究团队凭借自主研发的SMT独立求解器Xolver荣获“单查询赛道最大贡献——不可满足性”（Single Query Track Largest Contribution——UNSAT Performance Winner）与“非线性整数实数算术”（QF_NIRA Winner）两项冠军。主要完成人为特别研究助理贾富琦，指导教师为马菲菲研究员与张健研究员。
Xolver采用“研究人员主导、AI编码智能体协同”的研发模式。研究人员负责总体架构、算法设计、任务组织及测试验证，Claude、ChatGPT、Kimi等AI编码智能体协同承担主要代码实现工作。为保障求解结果的可靠性，Xolver对可满足结果进行原始公式回验，并对部分不可满足性推理进行一致性检查。Xolver前端基于团队此前研发的SOMTParser，该组件负责SMT-LIB解析、类型检查和表达式管理等基础功能。
SMT求解器是形式化验证的基础引擎，广泛用于计算机基础软硬件的测试、分析与验证。SMT-COMP作为国际权威的SMT求解器竞赛，旨在对SMT求解器在不同逻辑理论上的求解能力与效率进行统一评测。此届SMT-COMP 2026吸引了Z3、cvc5、Bitwuzla、Yices2、OpenSMT等国际主流SMT求解器参赛，参赛团队来自微软研究院、斯坦福大学、爱荷华大学、SRI International等国际知名高校和科研机构。
Xolver开源项目网址：
https://github.com/fuqi-jia/Xolver
SOMTParser 开源项目网址：
供稿：基础软件与系统重点实验室
END
