By default, CVC4 cannot handle division in linear integer arithmetic logics like
QF_LIA (what Rumur speaks by default). The option --rewrite-divk makes it try a
work around for division by constants or other manageable quantities by
rewriting division into other operations.

It's still not capable of handling the full expression space of division, but I
don't think we should bail out on encountering an unsupported division
expression because other SMT solvers like Z3 can manage these. For now an
unsupported division expression results in a failing call to CVC4. However, the
failure is invisible unless you pass --debug.

The rest of the development of this feature can take place on master.

This should avoid reintroducing issues like those fixed in
d2949e35 and
1a734295.

d2949e35 introduced a bug wherein the raw value
written to a handle then passed to a function call was computed incorrectly. The
problem was essentially that additions and subtractions were swapped for calls
to ADD and SUB without noting that the latter actually write to their
destination.

Interestingly this was not caught directly by anything in the test suite but was
detected by GCC issuing -Wsign-compare warnings for the model
out-of-range-function-parameter2.m.

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"