Arie Gurfinkel

@LinerSu looks cool. At this point, I only care about performance. Precision is expected to be very low.

Right, the instructions are a bit outdated. They are mostly there for us to remember what packages are required. We would gladly accept a PR to fix this.

because they both resolve to @g.ptr

The pointer you have is to mem-ssa that computes memory SSA form of the program. That code might silently assume that a function has a designated exit basic block. Functions...

I am not sure what exactly you are referring to. SeaDsa provides a generic way to provide specifications to external functions. We provide such specification to `realloc`. It is not...

` --horn-shadow-mem-optimize=true` only works when all functions are inlined. Please set it to false when inlining is not enabled. I will leave the issue open since this is something that...

In Z3, the relevant API start here: https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h#L2996 In Boolector, look for operators that end with `o`. Like this one: https://github.com/Boolector/boolector/blob/master/src/boolector.h#L1154

@danblitzhou can we close this PR?

We have a local solution. @hgvk94 is working on cleaning it up before it can be submitted to master

Looks like something unexpected happens in model compression