This is a bit of a happy accident here. I thought we were explicitly requiring
the step of a for loop to be a generation-time constant, as CMurphi does.
However, it turns out we were actually constant folding the step during
validation, and as a side effect throwing an error during constant folding when
we encountering something non-constant.

This commit fixes validation to only attempt constant folding of the step when
it is actually foldable. We still need some generated validation checks for
loops that have dynamic bounds and/or steps.

Note that it is not yet possible to construct such a thing because validation
rejects for-loops with steps that are not generation-time constants.

Github: related to #164 "loop iteration code incorrect"

Github: related to #164 "loop iteration code incorrect"

The synthesised types for quantified variables were not being considered when
calculating MAX_SIMPLE_WIDTH. This was in turn used within some assertions in
generated code about the maximum size of a handle read or write. A loop with
non-constant bounds induces a type with range [INT64_MIN, INT64_MAX] which often
exceeds the width of any other type in the model. As a result, such a model
would cause the handle width assertions to fail. Because these assertions become
assumptions in non-debug mode, they would cause incorrect execution when
debugging was turned off.

Github: closes #165 "MAX_SIMPLE_WIDTH considered harmful?"

We're about to need to override more than just the type visitors.

Github: related to #164 "loop iteration code incorrect"

The generated code for a loop (stemming from either a for statement, a forall
expression, or an exists expression) was surprisingly completely broken. When
not iterating over a type (`for x: mytype do ...`) but rather a range
(`for x := 0 to 10 ...`), the generated code would not perform the correct
number of iterations. With ranges not starting from 0, the problem would be
compounded and the value of the loop counter would be incorrect.

This bug was picked up while doing some unrelated work on quantifiers. The fact
that it has never been reported by a user and does not seem to cause any issues
in the test suite or production models leads me to think range-based for loops
are not very common.

Note: down-counting loops (e.g. `10 to 0 by -1`) still do not yet work.

Github: closes #164 "loop iteration code incorrect"
Github: related to #163 "reverse for ranges don't work"

Consider a range-based for loop:

  for i := 0 to 10 do
    ...
  end;

The variable used for i is constructed as an unbounded Range type. The bounds
for this default to [INT64_MIN, INT64_MAX] currently. By not taking this into
account, the logic that automatically selects a value_t was sometimes choosing a
smaller type (e.g. uint8_t). This resulting in reading and writing a handle that
exceed the width of value_t. This causes an assertion failure in debug mode and
incorrect optimisation in non-debug mode.

This is not yet a complete fix. We also need to more precisely bound the type of
the loop variable itself, as its width will currently always exceed the width of
value_t.

We now have references to quantified variables resolving to something
non-transient. The motivation for this was to make the SMT bridge's life easier
but this actually leads to more overall consistency as well.

The eventual aim here is to allow references to quantified variables to resolve
to a first class VarDecl.

We'll need quantifiers to deal with forall handling that is upcoming.

Note that the down-count iteration actually still fails and has been left
disabled. This little excursion exposed an extra bug here.

Github: related to #163 "reverse for ranges don't work"

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.