xazax.hun added a comment.

In D120289#3341008 <https://reviews.llvm.org/D120289#3341008>, @sgatev wrote:

> it seems tailored to the Z3 API.

As far as I understand, there were downstream patches that used the same API 
with other SMT solvers. The authors did not upstream it because they did not 
see any major improvement on Z3 for any of the use cases.

> What do you think about this? Any other options we should consider?

After reading your analysis, I'm fine with the current approach.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D120289/new/

https://reviews.llvm.org/D120289

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to