[Question]: How to get learnt clause while solving formula in z3?

[hagozaebii]

Hello,

Recently, I got questions about CDCL in z3. The questions are as follows:

1. I want to observe the clauses learned through the CDCL algorithm in real-time during formula solving. Is there a way to show these learned clauses in z3? Specifically, I'm curious if there's a python API that enables monitoring of the clause learning process. Any insights on how to track the learning of the clause database during solving would be greatly appreciated.

2. When I use -st option, I can see mk-clause. Is it learnt clause in CDCL? If not so, could you let me know how to get information about learnt clause?

Thank you for your time!