smt2: flatten FPA-encoded floats to their IEEE bit pattern

[tautschnig]

smt2_convt::flatten2bv is reached when a value has to be turned into a plain bit-vector, e.g. at a union/byte-access (type-punning) boundary. For a floatbv operand encoded with the SMT-LIB FloatingPoint theory it previously asserted !use_FPA_theory and gave up, because that theory has no float-to-bit-vector operation. As a result any program that reads the raw bytes of an FPA-encoded float under an FPA solver (--cprover-smt2, or --z3/--cvc5/--bitwuzla with --fpa) hit an invariant violation -- for example reading a double's bit pattern via a union { double d; uint64_t i; }.

Two shapes cover the cases that actually arise from type-punning, and both are emitted without needing a float-to-bit-vector operation:

• a constant: the IEEE interchange bit pattern is exactly the value's bit-vector representation, so it is emitted as a literal bit-vector;
• a bit-pattern reinterpret (float)bits (a typecast from a same-width generic bit-vector, as produced when lowering byte operators): flattening recovers precisely those bits, i.e. the typecast operand.

A non-constant FPA float that is not such a reinterpret would require the bvfromfloat round-trip (a fresh bit-vector b with to_fp(b) = x), which has to be registered by find_symbols; that case does not arise from the byte-/union-lowering paths and is left as a clearly-reported unsupported case rather than the previous blanket invariant.

SAT mode is unaffected: use_FPA_theory is false there, so the existing convert_expr(expr) path is taken unchanged.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR updates smt2_convt::flatten2bv to support flattening floatbv expressions when using the SMT-LIB FloatingPoint (FPA) theory, addressing crashes when a program type-puns floats (e.g., union/byte-access to read IEEE bit patterns) under --smt2 --fpa.

Changes:

• Add an FPA-specific flatten2bv path for floatbv that can emit IEEE bit-pattern bit-vectors for float constants.
• Recognize and flatten the common “bit-pattern reinterpret” shape (float)bits by emitting the underlying same-width bit-vector operand.
• Replace the previous blanket !use_FPA_theory invariant with a narrower “unsupported shape” failure for non-constant, non-reinterpret FPA floats.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

❌ Patch coverage is 96.07843% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.60%. Comparing base (5453820) to head (ee629cf).

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

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9031   +/-   ##
========================================
  Coverage    80.60%   80.60%           
========================================
  Files         1711     1711           
  Lines       189466   189515   +49     
  Branches        73       73           
========================================
+ Hits        152719   152762   +43     
- Misses       36747    36753    +6     

☔ 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.

[kroening]

Can this be generalised beyond constants by using the FPA to bit vector conversion operator?

[tautschnig]

Can this be generalised beyond constants by using the FPA to bit vector conversion operator?

The general case is already handled via bvfromfloat, and this current UNEXPECTEDCASE is really unreachable as every non-constant path of such a conversion will be subject to lower_byte_operators, which produces float typecasts, which in turn will be handled by bvfromfloat.

If we want to handle some future scenario where such a non-constant conversion would not be subject to lower_byte_operators this is doable, but it seems to be considerable extra work.

[kroening]

Ok, at the very least the description should be changed; the SMT-LIB FP theory does have a float-to-bit-vector operator, namely
((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

[kroening]

And I would probably add some narrative why these aren't used.

[tautschnig]

And I would probably add some narrative why these aren't used.

Good point — fixed the wording. fp.to_ubv/fp.to_sbv are value conversions (round to integer; undefined on NaN/∞/out‑of‑range), not the IEEE‑754 bit‑pattern reinterpret, and SMT‑LIB has no standard inverse of (_ to_fp …). Updated the comment, commit message and test docs to say that and why those operators aren't used.