z3-plus-plus.github.io

View My GitHub Profile

Z3++

Overview

Z3++ is a derived SMT solver based on Z3. It participates in the SMT-COMP 2022, and significantly improves Z3 on the following logics:

QF_IDL, QF_LIA, QF_BV, QF_NIA and QF_NRA

It is a project mainly developed in State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China.

Detailed description and source code are available at the github repository.

Contact

z3_plus_plus@outlook.com

Awards

At the FLoC Olympic Games, Z3++ won 2 gold medals (6 in total) for Biggest Lead Model Validation and Largest Contribution Model Validation.

People

Leader:

Shaowei Cai.

Team Members:

Bohan Li,

Jinkun Lin (SeesMaas Inc.),

Zhonghan Wang,

Bohua Zhan,

Xindi Zhang,

Mengyu Zhao.