I would like to see what patterns Z3 is using for some quantifiers in my formulas.
This comment suggests that it may be possible, but I couldn't find any more details.
How do I get Z3 to print this information?
Based on a helpful comment from Christoph, I found that building Z3 in debug mode (pass -d to mk_make.py during the build process) and then passing -v:10 on the command line to the resulting Z3 prints inferred patterns.