kparzysz added a comment. Btw, earlier on I found this paper, but I decided against it because it wouldn't solve inequalities: https://arxiv.org/abs/1507.07513 (and it would be more work...). Repository: rL LLVM https://reviews.llvm.org/D48283