Fix flattened overflow_result_exprt field order in SMT2

[fcasal]

Fixes #9144.

Problem

overflow_result_exprt has the struct type { value, overflow-<kind> }.
When SMT-LIB datatypes are unavailable, smt2_convt flattens that struct
into a bit-vector with value in the low bits and the overflow flag above
it.

Signed add/sub and signed/unsigned multiply emitted the fields in the
opposite order. Member access then returned the wrong result and overflow
flag, causing both false counterexamples and missed overflows.

Change

The affected paths now emit:

(concat overflow_flag result)

instead of:

(concat result overflow_flag)

The patch updates:

• signed addition and subtraction
• signed multiplication
• unsigned multiplication

Unsigned addition and subtraction were already correct: their extended
sum has the result in the low bits and the carry-out above it.

The refactoring builds the overflow predicate once and then uses it in the
datatype, flattened-result, or boolean-only output. Datatype output and
boolean-only overflow checks are unchanged.

Tests

Unit test

unit/solvers/smt2/smt2_conv.cpp checks the emitted SMT2 for:

• the four corrected cases
• unsigned add/sub, which were already correct
• boolean-only overflow expressions
• the datatype encoding used by Z3/CVC5

Reverting the fix makes only the four corrected sections fail. The focused
Catch run reports 4 of 22 assertions failed.

Regression tests

overflow-result-flattening1 checks ten assertions across unsigned
multiply/add and signed multiply/add/sub. Before the fix, seven failed
spuriously under CPROVER SMT2 and Bitwuzla.

overflow-result-flattening2 checks the opposite direction:
0x10000u * 0x10000u must overflow and may truncate to zero. Before the
fix, affected back-ends missed both failures.

Both tests are CORE no-new-smt, so they exercise the default SAT,
CPROVER SMT2, Bitwuzla, and Z3 paths while excluding the unsupported
incremental SMT2 back-end.

Verification

With the fix, all four tested back-ends agree:

Test	SAT	CPROVER SMT2	Bitwuzla	Z3
no false failures	0/10	0/10	0/10	0/10
expected failures found	2/2	2/2	2/2	2/2

Additional checks:

• focused SMT2 unit suite: 213 assertions in 40 test cases pass
• full default-SAT regression suite: pass, 67 skipped
• full CPROVER-SMT2 regression suite: pass, 112 skipped
• full Z3 regression suite: one unrelated flaky Function4 failure; it
  passes in isolation and with unmodified CBMC 6.8.0/6.9.0
• downstream Kani crypto-bigint harness: Bitwuzla and Z3 agree across all
  40 properties after the fix

To run the focused checks:

$ cmake --build build --target cbmc unit smt2_solver
$ ./build/bin/unit '[core][solvers][smt2]'
$ cd regression/cbmc
$ make test
$ make test-cprover-smt2

[codecov]

Codecov Report

❌ Patch coverage is 95.74468% with 4 lines in your changes missing coverage. Please review.
✅ Project coverage is 81.42%. Comparing base (a777c7b) to head (e36c27d).

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	88.57%	4 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9145      +/-   ##
===========================================
+ Coverage    80.83%   81.42%   +0.58%     
===========================================
  Files         1715     1715              
  Lines       189989   211534   +21545     
  Branches        73       73              
===========================================
+ Hits        153576   172236   +18660     
- Misses       36413    39298    +2885     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.