As per [0], source only uploads are preferred. I believe they are now required
for migration out of testing [1]:

  From now on, we will no longer allow binaries uploaded by maintainers to
  migrate to testing. This means that you will need to do source-only uploads if
  you want them to reach bullseye.

  [0]: https://wiki.debian.org/SourceOnlyUpload
  [1]: https://lists.debian.org/debian-devel-announce/2019/07/msg00002.html

Github: related to #85 "release beta"

Merge commit '58d8e07b'; commit 'dafb1e3c'

The motivation for this is to support Debian's autopkgtest which wants to be
able to run the test suite against an *installed* copy of the binaries.

Github: related to #85 "release beta"

The motivation for this is to support Debian's autopkgtest which wants to be
able to run the test suite against an *installed* copy of the binaries.

Github: related to #85 "release beta"

When you create an unstable environment by installing a stable ISO and then
switching package sources, lsb_release still claims you are on stable so this
check fails.

When you create an unstable environment by installing a stable ISO and then
switching package sources, lsb_release still claims you are on stable so this
check fails.

The initial allocation of each thread-local allocator pool was intended to be
close to 8MB. However, the calculation was using the sizeof a pointer rather
than the state structure itself. As a result, the initial allocator pool was
typically much larger than 8MB.

Github: closes #157 "initial arena size incorrect?"

These functions do not set errno, but instead return an errno.

We're no longer intending to take advantage of this.

This reverts commit 1100fae5. It turns out that
some SMT solvers don't stick to the constraints of the logic and happily accept
expressions outside of it. So we would like to still emit things that may be
outside the given logic in case the solver understands them.

The particular situation that motivated this is that Z3 does not understand the
logic QF_ALIA and falls back to its behaviour of accepting a superset of the
logics it knows. This means that, e.g., switching from QF_ALIA to QF_AUFLIA
makes some problems unsolvable because Z3 *does* know QF_AUFLIA and imposes
further restrictions.

We really should have been using a UF logic already, given we generate
declare-fun commands. However, seems most solvers are happy to accept these in
non-UF logics as well.

Github: closes #153 "unresolved TypeExprIDs with differing names are considered
  equal"

This was just replicating the functionality of TypeExpr::coerces_to.

Slightly more accurate name.

Because the lexer is caseless, we get this for free even though it looks like we
don't.

Github: closes #156 "FreeBSD CI testing"

When using an SMT logic like QF_LIA (`--smt-logic QF_LIA`) with no support for
arrays, the SMT bridge would translate models containing array expressions. This
meant the SMT solver would receive a problem it would not understand. We now
bail out of translation when encountering an array expression while using a
logic that does not support arrays.

Github: related to #151 "variable shadowing causes invalid SMT problems"

Instead of translating a variable like "foo" into something like "ru_foo" in the
SMT bridge, we translate it to something like "s23". The purpose of this is to
support symbol shadowing. E.g. in Murphi you can declare a rule-local variable
that shadows one of the state variables. In translation to SMT this previously
resulted in a malformed problem with a duplicate symbol definition.

It would have been possible to work around this using scoping in SMT (`push` and
`pop` commands) but these are not supported by all solvers. Instead we stop
relying on the uniqueness of the Murphi symbols and construct unique symbols out
of the AST identifiers. This makes the SMT problem less readable but more often
syntactically well formed.

Note that a side effect of this change is that Murphi identifiers that use
characters not understood by your SMT solver (e.g. UTF-8 accented letters) no
longer cause malformed SMT problems.

Github: closes #151 "variable shadowing causes invalid SMT problems"

Previously we were "unwrapping" a TypeDecl during symbol resolution. This meant
that later on there was no way to ask "what TypeDecl did this TypeExprID point
at?" This question was previously irrelevant but we now need to start
synthesising unique symbols in the SMT bridge and it's becoming necessary.

Performing simplification within the referent of a TypeExprID is only useful if
we intend to emit pieces of the referent during eventual code generation. This
is not the case currently.

This should ensure that resolved ExprIDs always have a referent with a valid
unique identifier.

We're going to need unique identifiers for the enum members in the SMT bridge.

I had some doubts as to the semantics of this when I omitted these constructs to
begin with, but it was confirmed by GCC ≥ 4.7 leveraging this to make
model-breaking optimisations. We now conservatively consider any property
statement or error statement to be an indicator of impurity.