中国科学院软件研究所 · 基础软件与系统重点实验室 · 基础软件测试与分析研究室
SMT-COMP 2026 · 双项冠军
自主研发 SMT 求解器 Xolver
荣获国际 SMT-COMP 2026 两项冠军
软件测试与分析研究室研究团队凭借自主研发的 SMT 独立求解器 Xolver，
在国际权威 SMT 求解器竞赛 SMT-COMP 2026 中取得两项冠军。
01
UNSAT PERFORMANCE WINNER
单查询赛道最大贡献——不可满足性
Single Query Track Largest Contribution—UNSAT
Single Query Track Largest Contribution—UNSAT
02
QF_NIRA WINNER
非线性整数实数算术
QF_NIRA Winner
QF_NIRA Winner
近日，2026年度国际 SMT 求解器竞赛（SMT-COMP 2026）公布结果。
中国科学院软件研究所基础软件与系统重点实验室基础软件测试与分析研究室研究团队
凭借自主研发的 SMT 独立求解器 Xolver，
荣获“单查询赛道最大贡献——不可满足性”
（Single Query Track Largest Contribution—UNSAT Performance Winner）
与“非线性整数实数算术”（QF_NIRA Winner）两项冠军。
主要完成人 贾富琦
指导教师 马菲菲 研究员
指导教师 张健 研究员
研究人员主导 · AI 编码智能体协同
HUMAN-LED · AI-COLLABORATIVE DEVELOPMENT
Xolver 采用“研究人员主导、AI编码智能体协同”的研发模式。
研究人员负责总体架构、算法设计、任务组织及测试验证，
Claude、ChatGPT、Kimi 等 AI 编码智能体协同承担主要代码实现工作。
面向可靠求解的技术设计
RELIABILITY BY DESIGN01
原始公式回验
为保障求解结果的可靠性，Xolver 对可满足结果进行原始公式回验。
02
一致性检查
对部分不可满足性推理进行一致性检查，进一步增强求解结果可信度。
03
SOMTParser 前端
Xolver 前端基于团队此前研发的 SOMTParser， 负责 SMT-LIB 解析、类型检查和表达式管理等基础功能。
国际权威 SMT 求解器竞赛
SMT-COMP 2026
SMT 求解器是形式化验证的基础引擎，广泛用于计算机基础软硬件的测试、分析与验证。
SMT-COMP 作为国际权威的 SMT 求解器竞赛，
旨在对 SMT 求解器在不同逻辑理论上的求解能力与效率进行统一评测。
此届 SMT-COMP 2026 吸引了 Z3、cvc5、Bitwuzla、Yices2、OpenSMT 等国际主流 SMT 求解器参赛， 参赛团队来自微软研究院、斯坦福大学、爱荷华大学、 SRI International 等国际知名高校和科研机构。
此届 SMT-COMP 2026 吸引了 Z3、cvc5、Bitwuzla、Yices2、OpenSMT 等国际主流 SMT 求解器参赛， 参赛团队来自微软研究院、斯坦福大学、爱荷华大学、 SRI International 等国际知名高校和科研机构。
Z3
cvc5
Bitwuzla
Yices2
OpenSMT
Microsoft Research
Stanford University
University of Iowa
SRI International
开源项目
OPEN SOURCESMT Solver
Xolver
自主研发 SMT 独立求解器，SMT-COMP 2026 两项冠军。
github.com/fuqi-jia/Xolver
SMT-LIB Frontend
SOMTParser
面向 SMT-LIB 的解析、类型检查与表达式管理基础组件。
github.com/fuqi-jia/SOMTParser
以自主基础软件能力，探索 形式化方法 × AI 的新型研发路径
SOFTWARE TESTING & ANALYSIS RESEARCH · INSTITUTE OF SOFTWARE, CAS