In CI the test script thinks the system locale is ASCII, but apparently one of
the subprocesses gives us non-ASCII data. Rather than trying to deal with this
mess, just ignore encoding errors when piping data back to stdout/stderr.

Github: related to #142 "pending-queue.m terminates exploration too early"

This was leading to the misc/pending-queue.m model terminating early with a
surprisingly small number of states. Some more explanation from the Github
issue:

  The misc/pending-queue.m model produces many fewer states (81) than it used to
  (147487952), which is unexpected. Bisecting indicates 79579fd5 is the first bad
  commit.
  ...
  The problem here is that commit 79579fd5 inadvertently caused the comparison in
  the loop emitted for a quantifier to become unsigned. A quantifier emits code
  that previously looked something like:

    const value_t step = VALUE_C(1);
    const value_t lb = VALUE_C(-1);
    const value_t ub = VALUE_C(3);
    for (value_t _ru1_i = lb; _ru_i <= ub; _ru_i += step) {
    ...

  After that commit, the emitted code looks like:

    const raw_value_t step = (raw_value_t)1;
    const raw_value_t lb = (raw_value_t)VALUE_C(-1);
    const raw_value_t ub = (raw_value_t)VALUE_C(3);
    for (raw_value_t _ru1_i = 1; _ru_i <= ub - lb + 1; _ru_i += step) {
    ...

  Now everything generally works out fine except in cases like the above when
  the range spans positive and negative values. Notice that the first iteration
  of the loop in the second case already has a false condition. The problem here
  is that the comparison was previously comparing value_ts and now it's
  comparing raw_value_ts. In a typical model this goes from comparing int8_t
  values to uint8_t values.

Github: closes #142 "pending-queue.m terminates exploration too early"

Github: related to #142 "pending-queue.m terminates exploration too early"

Now that Rumur itself doesn't use this, there seems little point to preserve
this when a client can implement it themselves as a simple traversal.

Github: related to #141 "segfault with misc/pending-queue-4k.m"

7dda1203 changed the way global assumptions were
emitted to return a boolean rather than signaling assumption failure via
siglongjmp. Following this, 603f1809 optimised
sigsetjmp calls to be skipped if max errors was 1, even if there were
assumptions in the model. The reasoning here was that assumptions were now using
regular control flow via returns, so didn't require a jmp_buf. The problem with
this is that assumption *statements* are still using siglongjmp.

The effect of these combined changes was that models that failed assume
statements would attempt to siglongjmp with an invalid jmp_buf causing a
segfault. On a debug verifier, this would become an assertion failure.

We repair this by now treating jmp_bufs as required if there are any assume
statements in the model. Note that this partially reverts
603f1809.

Github: closes #141 "segfault with misc/pending-queue-4k.m"

Github: related to #141 "segfault with misc/pending-queue-4k.m"

Github: related to #141 "segfault with misc/pending-queue-4k.m"

It's actually incorrect that this is unused, but we need to implement a more
nuanced version of this.

Github: related to #141 "segfault with misc/pending-queue-4k.m"

Github: related to #141 "segfault with misc/pending-queue-4k.m"

Note, this probably breaks for DragonFly and NetBSD that don't have sandboxing
options. We should disable this test for them before the next release.

This removes the need to lean on our hacky toy SMT solver going forwards.

GCC 4.7 apparently does not understand C++11 attributes.

We can't explicitly mark this deprecated because it triggers compiler warnings
when calling the implicit copy constructor from within Ptr's copy constructor.

This means ExprID::referent->is_in_state() is now usable as the offset
information within referents is consistent in a way
ExprID::referent->state_variable is not.

The latter was probably introduced too hastily and doesn't make for a good API.
We would like to have the freedom to change how we decide whether something is
in the state.

The purpose of this is to ensure that resolved symbols (e.g. ExprID::referent)
have the same final index as their original target declaration.

The offset calculation did not have much to do with reindexing and I think it
may have just been put here because it was a convenient post-resolution place
for it. An unfortunate side effect of this design was that resolved referents
had an invalid offset. To see why this is, note that symbol resolution (1)
replaces null referents with a *copy* of the target node and (2) runs prior to
reindexing. That is, the offset calculation in reindexing would only affect the
original state VarDecl, not its copies in ExprID referents.

None of what has just been described was a bug. The offsets of the VarDecl
copies are never used. But its presence incorrectly suggests to librumur clients
that it is usable.

In this commit we move the offset calculation to its more natural place within
symbol resolution. We do offset calculation *prior* to declaring a VarDecl in
the symbol table. This results in ExprIDs now receiving a referent with correct
offset information. Note that we need to do some extra checks because a
just-parsed VarDecl is part of an unvalidated model and may be invalid.

All this is part of a broader direction to make all the fields of a referent
valid and usable.

This will be removed in a future release.

This is the equivalent of validate_model, but for *any* node in the AST.

We're about to introduce a function for validating any subpart of the AST. That
is, effectively calling validate_model with a node other than the topmost node.
This means that the referent of a reference node (ExprID, FunctionCall or
TypeExprID) may not yet have been validated. So we need to drop the optimization
that avoids descending into these.

This makes validating a model take longer, but the difference should be
negligible. If this becomes a problem, we could start memoising visitor
dispatch.

The AST node indices (unique_id) are not used by the dump utility, so reindexing
is unnecessary.