Michael Emmi

> Would dependencies such as Corral be packaged as well? Yes, we’d have to figure out how to do that. The end result should be that `brew install smack` results...

> I have never seen anyone use homebrew on Linux. This is still pretty new, so not surprised that we don’t know people using it (especially in academia). And while...

Update: I‘ve got this working completely on MacOS by following [this blog post](https://jonathanchang.org/blog/maintain-your-own-homebrew-repository-with-binary-bottles/) and lifting [these workflows](https://github.com/jonchang/homebrew-biology/tree/master/.github/workflows) from the same author. Long story short: on macOS Catalina you can run...

Note: it is the --mem2reg flag, which we pass to llvm, that ultimately introduces these "undefined" values.

At the moment, the only way I see to resolve this issue is to disable LLVM's mem2reg pass, which I advise against, due to the mess of additional memory operations...

According to the LLVM reference manual, each "undef" should correspond to a unique uninitialized value, so actually the previous comment is irrelevant.

I can imagine this being implemented in a few ways, with varying degrees of possibly-premature optimization. The first would be to encode LLVM vectors with Boogie maps. For instance, ````...

By the way, since the mask argument to `shufflevector` is a constant vector, we can optimize our encoding by creating a distinct `$shufflevector` function for each distinct mask. For instance,...

Agreed, this should definitely be done!

Is it possible to write a C-language test case for this?