I am willing to do this. I used to write a tool that extracts boolean expressions from an LLVM IR corpus and use Alive2 to check whether they are tautology or unsatisfiable: llvm-tools/deadcode.cpp at main · dtcxzyw/llvm-tools · GitHub
It has discovered some missed optimization opportunities: Issues · dtcxzyw/llvm-tools · GitHub
I think it is easy to extend the tool to support dominating conditions.