Hi, I just noticed that Z3 was integrated into the clang frontend to solve some kind of constraints: https://reviews.llvm.org/rL299463 What kinds of constraints are these, i.e. which problem are they solving, and is there a possibility of running into an exponential runtime? Kind regards, -- Paulo Matos