minor: recover README

README.md

@@ -1,3 +1,19 @@
+# Z3++
+
+Z3++ is a derived SMT solver based on Z3, by combining local search and preprocessing techniques into Z3.
+Z3++ won the gold for Biggest Lead Model Validation and Largest Contribution Model Validation in SMT-COMP 2022 and 2023.
+
+For any solver built upon Z3++, we would appreciate that the solver includes "Z3++" in the name for credit.
+
+The homepage of Z3++ is http://z3-plus-plus.github.io/
+
+Reference can be found as follows:
+
+Shaowei Cai, Bohan Li, Jinkun Lin, Bohua Zhan, Xindi Zhang, Mengyu Zhao. "Z3++ at SMT-COMP 2023"
+
+Shaowei Cai, Bohan Li, Xindi Zhang. "[Local Search For SMT on Linear Integer Arithmetic.](https://link.springer.com/chapter/10.1007/978-3-031-13188-2_12)" In CAV 2022
+Shaowei Cai, Bohan Li, Xindi Zhang. "[Local Search For Satisfiability Modulo Integer Arithmetic Theories](https://dl.acm.org/doi/10.1145/3597495)" In ACM Transactions on Computational Logic 2023
+
 # Z3
 
 Z3 is a theorem prover from Microsoft Research.