Shaobo

Symbooglix has a pass to remove unused axioms and declarations. Although that pass is buggy, since we add Symbooglix to the support, can we add an option to invoke this...

Btw, for the attached file, if I invoke it with `smack enclave.so.ll --entry-point printf` Corral also throws the same exception. [enclave.so.txt](https://github.com/smackers/smack/files/5285877/enclave.so.txt)

If we decide to do so, we have to make sure that our implementation of `malloc` returns before the actual body. I saw interesting bug like the custom `malloc` calls...

Some background information about sea-dsa: sea-dsa's context-sensitive analysis produces a graph for each function, where each pointer of the function is associated with a cell. Take one of sea-dsa's regression...

> I don't quite understand what this pass does. Could you add extensive comments into the pass describing what exactly it does? Also, copy them here too. Thx! Sorry for...

Hello @muyaview, It appears the spurious counterexample is not a result of the `--bit-precise` flag. The real reason is that SMACK models the operation `store.vec.4xbv32.bv8` using unintepreted functions. So, I'm...

> Hi @shaobo-he , > > Thanks for your clarification. Apart from warning this unsoundness, if it is possible to fix this to handle the operation correctly? I'm not sure....

> Could you please resolve conflicts @shaobo-he ? Thanks! Done.

@jjgarzella is this issue resolved?

> @shaobo-he As far as I know, no. For example the VMCAI artifact uses the workaround with the manual command line option. > > However, this only really affects Kotlin...