smt2: support bit-pattern reinterpretation overload of to_fp

[tautschnig]

The SMT-LIB FloatingPoint theory's to_fp is overloaded. All overloads but one take a rounding mode followed by a source operand; the exception is the bit-pattern reinterpretation

((_ to_fp eb sb) (_ BitVec eb+sb))

which takes a single bit-vector operand and no rounding mode, and interprets those bits directly as the IEEE-754 interchange encoding. CPROVER's smt2 parser unconditionally read a rounding mode and a source operand, so it rejected this form with "unexpected token in an expression".

This overload is what CBMC itself emits for the bvfromfloat round-trip (constraining a fresh bit-vector b by ((_ to_fp e f) b) = x) and for unflattening an FPA result of a bit-vector float helper, so the legacy --cprover-smt2 backend could not solve any problem that read the bit pattern of an FPA-encoded float (e.g. type-punning a double to its bit pattern via a union).

The handler now parses the first operand, then peeks: if the form closes there it was the single bit-vector operand of the reinterpretation, which is modelled as a bit-level reinterpret (a typecast through a generic bit-vector type, which boolbv_typecastt treats as a reinterpret rather than a numeric conversion); otherwise the first operand was the rounding mode and a source operand follows, exactly as before.

A new regression/smt2_solver test exercises the overload directly.

• 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 fixes the SMT2 parser’s handling of the SMT-LIB FloatingPoint theory’s overloaded to_fp operator by adding support for the single-operand bit-pattern reinterpretation form ((_ to_fp eb sb) (_ BitVec eb+sb)). This enables the legacy --cprover-smt2 backend to accept and solve problems that reinterpret IEEE-754 interchange-encoded bit-vectors as floating-point values.

Changes:

• Extend smt2_parsert::function_application() to detect whether ((_ to_fp eb sb) ...) closes after the first parsed operand and, if so, model it as a bit-level reinterpret cast instead of a rounding-mode + source conversion.
• Add a new regression/smt2_solver test exercising the single-argument to_fp overload and expecting unsat.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/solvers/smt2/smt2_parser.cpp	Adds parsing + internal modelling for the to_fp bit-pattern reinterpretation overload by peeking for immediate close after the first operand.
regression/smt2_solver/fp/bit-to-fp2.smt2	New SMT2 regression that reinterprets the IEEE-754 bit pattern of 1.0 using the single-operand to_fp overload.
regression/smt2_solver/fp/bit-to-fp2.desc	Registers the new regression test and checks for unsat output.

---

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

[codecov]

Codecov Report

❌ Patch coverage is 80.00000% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.60%. Comparing base (23d2707) to head (c39ebd0).

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

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9032   +/-   ##
========================================
  Coverage    80.60%   80.60%           
========================================
  Files         1711     1711           
  Lines       189454   189464   +10     
  Branches        73       73           
========================================
+ Hits        152700   152709    +9     
- Misses       36754    36755    +1     

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