We now have full model content when piping in a model from stdin as well as when
the model arrives via a file.

It seems the stream that is used for parsing is unusable afterwards. Flex or our
own code has caused failbit to be set. Instead of trying to undo this, simply
use another stream. We'll make use of this for replay in an upcoming commit.

This is part of work towards including the input model content with the AST
produced by rumur-ast-dump, regardless of whether the model is provided in a
file or on stdin.

This was intended to be a parent of master already, but I seem to have somehow
fouled this up in a previous packaging cycle.

Github: closes #168 "add xmllint and an SMT solver to FreeBSD testing"

This is required to run the ast-dump tests.

Github: related to #168 "add xmllint and an SMT solver to FreeBSD testing"

When building in debug mode, the user could trigger an assertion failure by
setting a value type that was too small to contain values in the model. Note
that this would *only* occur when the user specifically overrode --value-type
with a narrower type than the one that would have been selected automatically.

Github: closes #166 "users can force verifier assertion failure"

We're about to introduce a new error case in these functions.

Github: related to #166 "users can force verifier assertion failure"

If value_t is chosen to be an unsigned type, comparisons like `v < 0` cause
warnings with -Wtype-limits. We also need to work around a -Wsign-compare bug in
this change.

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

We should now have full support for incrementing by negative amounts within a
quantifier.

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

The lower bound may be above the upper bound if the user has described a down
counting loop. These aren't properly supported yet, but it is an aspiration.

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

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.