Marek Surovič

Add more testsuites

2

Potential candidates: https://github.com/brenocfg/AnghaBench

[Smt-Switch](https://github.com/stanford-centaur/smt-switch) is a generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers, including Z3, CVC5 and more. This could provide access...

Investigate simplification using Z3's `ctx-solver-simplify`

1

In `rellic-decomp` we currently employ a our own Z3 simplifiers made of various Z3 tactics. This is done [here](https://github.com/lifting-bits/rellic/blob/96fc148723be33e1dcdca256d3f28d75dc4339c2/tools/decomp/Decomp.cpp#L240) and [here](https://github.com/lifting-bits/rellic/blob/96fc148723be33e1dcdca256d3f28d75dc4339c2/tools/decomp/Decomp.cpp#L280). However Z3 also contains `ctx-solver-simplify` which is a heavyweight...

Add proper handling of `undef` values

1

[https://llvm.org/docs/LangRef.html#undefined-values](url) Relates to #158

```c *(unsigned int *)*(unsigned int *)&_sroa_3_sroa_3[3U] + ((unsigned int)arg0

[input.zip](https://github.com/lifting-bits/rellic/files/6817601/input.zip)

Add LLVM IR based regression tests

1

Preprocessing with `llvm-reduce` is encouraged.

Related to [this TODO](https://github.com/lifting-bits/rellic/blob/76d8fa1787d2368a35f62e1f5884eef905f87ef8/rellic/AST/Z3ConvVisitor.cpp#L785)

My recommendation would be make all of these strings into global `std::string`that represent your "abi" of sorts for interfacing with z3. _Originally posted by @pgoodman in https://github.com/lifting-bits/rellic/pull/121#discussion_r633642031_ note: maybe try...