SMT2 back-end swaps fields in flattened overflow results

[fcasal]

Summary

overflow_result_exprt represents checked arithmetic as the struct
{ value, overflow-<kind> }.

SMT2 back-ends without datatype support flatten this struct into one
bit-vector. The expected layout is:

most significant                         least significant
[ overflow flag ][             value                      ]

Three emitters instead produce [ value ][ overflow flag ]:

• signed add/sub
• signed multiply
• unsigned multiply

The generic member accessor still reads value from the low bits and the
overflow flag from the high bit. It therefore reconstructs:

• value as (result << 1) | overflow_flag
• overflow as the top bit of the truncated result

This creates both false alarms and missed overflows.

Affected back-ends

Affected: Bitwuzla, Boolector, CPROVER SMT2, MathSAT, Yices, and generic
SMT2 output.

Not affected:

• Z3 and CVC5, which use SMT-LIB datatypes
• the default SAT back-end, which uses a separate encoding
• smt2_incremental, which does not support overflow_result_exprt

Reproducer: incorrect result

int main(void)
{
  unsigned int a, b, result;
  __CPROVER_assume(a < 4 && b < 4);

  int overflow = __builtin_mul_overflow(a, b, &result);
  __CPROVER_assert(!overflow && result < 16, "small product");
}

$ cbmc mulbug.c
VERIFICATION SUCCESSFUL

$ cbmc --z3 mulbug.c
VERIFICATION SUCCESSFUL

$ cbmc --bitwuzla --trace mulbug.c
VERIFICATION FAILED

The Bitwuzla trace includes a = 3, b = 3, and result = 18: the
correct result, 9, shifted left by one.

Reproducer: missed overflow

int main(void)
{
  unsigned int a, b, result;
  __CPROVER_assume(a == 0x10000u && b == 0x10000u);

  int overflow = __builtin_mul_overflow(a, b, &result);
  __CPROVER_assert(!overflow, "expected to fail");
}

0x10000 * 0x10000 is 2^32, so the assertion must fail. The default SAT
back-end and Z3 report the failure, but Bitwuzla reports
VERIFICATION SUCCESSFUL because it reads the overflow flag from bit 31 of
the truncated result, which is zero.

The same flattened formula produces the same incorrect answer in Z3, so
the problem is in CBMC's encoding rather than in Bitwuzla.

Kani impact

Rust arithmetic with overflow checks lowers to *_with_overflow intrinsics.
Kani harnesses are affected when those operations survive simplification and
reach this SMT2 path under --solver bitwuzla.

For example, a symbolic u32 constrained to 3 causes Bitwuzla to refute
a * a == 9, while Kani's SAT back-ends and Z3 verify it. A symbolic
0x10000u32 * 0x10000u32 overflow is missed in the opposite direction.

Observed with Kani 0.67.0, which bundles CBMC 6.8.0.

Versions

Reproduced with CBMC 6.8.0, 6.9.0, and commit a777c7b2. Signed and
unsigned multiplication are affected at every tested width
(u8/u16/u32/u64 and signed equivalents), as are signed addition and
subtraction. Unsigned addition and subtraction already use the correct
layout.

Proposed fix

Emit the overflow flag as the most-significant concat operand and the
result as the least-significant operand, matching convert_struct,
flatten2bv, and convert_member.