<div dir="ltr"><div><div>Hi all,<br><br></div>Base on the previous discussions on the cfe-dev mailing list and my personal research, I wrote a proposal for integrating z3 SMT solver with clang static analyzer. Base on George's advice, I would like the cfe-dev community to take a look at the proposal and give me some feedback. I do not have much experience with the Clang Static Analyzer so there might be some misunderstanding on my part, therefore any feedback is appreciated!<br><br><a href="https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing">https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing </a><br><br></div><div>Looking forward to your response,<br></div>Brenda<br><div><br></div></div>