Michael Emmi

Ah yes, the problem here is that you want to refer to the value returned from the function in the `ensures` specification. In general, this cannot be matched to a...

By the way, see [here](https://github.com/smackers/smack/blob/develop/lib/smack/SmackInstGenerator.cpp#L576) for the previous implementation of `result`.

It’s case sensitive.

Compare the result of running Boogie on this program ```` const M: [int] int; function {:inline} f(i: int) returns (int) { i } function {:inline} g(i: int) returns (bool) {...

Yes, it seems that MBQI might never terminate when the query is unsatisfiable.

Ah but we are issuing (some of) these warnings; for instance, here's an excerpt from the "globals" regression: $bb0: assume {:sourceloc "globals.c", 8, 18} true; call $p := $malloc($off($ptr($NULL, 4)));...

I tend to agree: the Boogie code we generate should probably be thought of as opaque, and not inspected by any Smack user. Therefore issuing warnings (only) there would not...

Might be a good idea to start with Ubuntu 18.

I would argue that figuring out how to build packages can be considered completely orthogonal its automation. So far I’ve looked a bit at Homebrew and Ubuntu. It appears that...

In the meantime I’ve been looking at creating [a Homebrew tap](https://github.com/smackers/homebrew-smack) with [a smack formula](https://github.com/smackers/homebrew-smack/blob/master/Formula/smack.rb) and [a workflow to create bottles](https://github.com/smackers/homebrew-smack/blob/master/.github/workflows/bottling.yml). It seems that [Homebrew on Linux](https://docs.brew.sh/Homebrew-on-Linux) might be an...