[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. In D54978#1457318 , @mikhail.ramalho wrote: > In D54978#1447107 , @gou4shi1 wrote: > > > My own out-of-tree pass `#include ` and use cmake's > > `add_llvm_library` to compile it into a `.

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. My own out-of-tree pass `#include ` and use cmake's `add_llvm_library` to compile it into a `.so` However, `opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll` fails: `opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: _ZN4llvm14CreateZ3SolverEv` (

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. > ! In D54978#1441547 , > @mikhail.ramalho wrote: > You can get the sort size by calling getBitvectorSortSize(). found, thx CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 _

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. > ! In D54978#1441417 , > @mikhail.ramalho wrote: > Sure, I'll create a new revision with the added functions tonight. I am very happy with your quickly reply. btw, `Z3_get_bv_sort_size` is also needed :) CHANGES SINCE LAST AC

[PATCH] D54978: Move the SMT API to LLVM

gou4shi1 added a comment. @mikhail.ramalho Can you plz add some wrappers of overflow predicates like Z3_mk_bvadd_no_overflow, Z3_mk_bvadd_no_underflow, ... to SMTAPI.h and Z3Solver.cpp? It could help me, thanks! CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://review