`--smt2 --outfile` aborts (flatten2bv: unsupported) on float↔int type-punning that native solving handles

[zhoulaifu]

Description

Exporting a formula with --fpa --smt2 --outfile aborts with an invariant violation as soon as the program reinterprets the bits of a non-constant float — e.g. the classic newlib union { float; unsigned; } / EXTRACT_WORDS / GET_FLOAT_WORD idiom:

flatten2bv of a non-constant FPA-encoded float is unsupported
src/solvers/smt2/smt2_conv.cpp:5001

The abort happens mid-write, leaving a truncated, unusable .smt2 file (header only, no (check-sat)).

Solving the same program natively (--fpa, no --outfile) succeeds and returns a verdict. The failure is specific to the SMT2 export path, not to the FP encoding itself.

The bit-reinterpretation idiom is pervasive in bit-exact libm code (e.g. the SV-COMP float-newlib suite), so for such programs --smt2 --outfile cannot produce a formula even though native solving handles them.

Reproducer (8 lines)

extern void reach_error(void);
extern float __VERIFIER_nondet_float(void);
int main(void) {
  float f = __VERIFIER_nondet_float();
  union { float f; unsigned u; } pun;
  pun.f = f;                          /* store non-const float, read its bits */
  if ((pun.u & 0x7fffffffu) > 0x7f800000u) reach_error();  /* NaN check via bits */
  return 0;
}

Steps to reproduce

1. Export to SMT2 — aborts

$ cbmc fp_bitpun_export_bug.c --fpa --smt2 --outfile /tmp/out.smt2
CBMC version 6.10.0 (cbmc-6.10.0) 64-bit arm64 macos
...
Outputting formula to file: /tmp/out.smt2
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: .../src/solvers/smt2/smt2_conv.cpp:5001 function: flatten2bv
Condition: Precondition
Reason: false
Backtrace:
4   cbmc   ... _ZN10smt2_convt10flatten2bvERK5exprt + 1588
5   cbmc   ... _ZN10smt2_convt6set_toERK5exprtb + 1828
6   cbmc   ... _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 220

Diagnostics:
<< EXTRA DIAGNOSTICS >>
flatten2bv of a non-constant FPA-encoded float is unsupported
<< END EXTRA DIAGNOSTICS >>
--- end invariant violation report ---

Exit code 134 (SIGABRT). The output file is truncated:

$ wc -c /tmp/out.smt2
1 /tmp/out.smt2
$ grep -c check-sat /tmp/out.smt2
0

The minimal trigger is exactly --fpa --smt2 --outfile; no other flags required.

2. Native solve, same program — succeeds

$ cbmc fp_bitpun_export_bug.c --fpa
...
SAT checker: instance is SATISFIABLE
[main.no-body.reach_error] line 7 no body for callee reach_error: FAILURE
** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

Expected vs actual

Expected: --smt2 --outfile writes a complete formula (with (check-sat)) for any program the native backend solves — or, if a construct is genuinely unsupported in the SMT2 backend, a graceful diagnostic with non-zero exit.

Actual: an internal invariant-violation abort (SIGABRT) mid-write, a 1-byte file, no (check-sat) — while the native path solves the identical program.

Version / platform

$ cbmc --version
6.10.0 (cbmc-6.10.0)
$ uname -mps
Darwin arm64 arm

CBMC 6.10.0, native macOS / Apple silicon.

Note

We also observe a distinct SMT2 export abort (same flatten2bv invariant) on array-of-floating-point-heavy programs with no bit-reinterpretation — a different trigger. Happy to open a separate issue with a minimal reproducer if useful.