Z3++ is a derived SMT solver based on Z3. It participates in the SMT-COMP 2022-2023, 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.
z3_plus_plus@outlook.com
SMT-COMP 2022: At the FLoC Olympic Games, Z3++ won 2 gold medals (6 in total) for Biggest Lead Model Validation and Largest Contribution Model Validation.
SMT-COMP 2023: Biggest Lead and Largest Contribution winner of Model Validation Track.
Bohan Li, Xindi Zhang, Mengyu Zhao.
Jinkun Lin (SeesMaas Inc.) (2022), Bohua Zhan (2022, 2023), Zhonghan Wang (2022)
[1] Shaowei Cai, Bohan Li, Xindi Zhang: Local Search for SMT on Linear Integer Arithmetic. CAV (2) 2022: 227-248
[2] Shaowei Cai, Bohan Li, Xindi Zhang: Local Search For Satisfiability Modulo Integer Arithmetic Theories. ACM Trans. Comput. Log. 24(4): 32:1-32:26 (2023)
[3] Bohan Li, Shaowei Cai: Local Search For SMT On Linear and Multi-linear Real Arithmetic. FMCAD 2023: 1-10
[4] Xindi Zhang, Bohan Li, Shaowei Cai: Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory. ICSE 2024
Z3++ 2022 (Shaowei Cai, Bohan Li, Jinkun Lin, Zhonghan Wang, Bohua Zhan, Xindi Zhang and Mengyu Zhao)
Z3++ 2023 (Shaowei Cai, Bohan Li, Bohua Zhan, Xindi Zhang, and Mengyu Zhao)
