[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

Wed Feb 23 16:07:16 PST 2022

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