https://github.com/NagyDonat commented: I added some inline comments; but I know almost nothing about the Z3 solver and related code, so I would be grateful if somebody with more knowledge would also review this change. https://github.com/llvm/llvm-project/pull/158276