smt2: do not declare UFs whose signature involves RegLan

[tautschnig]

find_symbols emits a (declare-fun ...) for every not-yet-seen function symbol, including the cprover_regex_* / to_regex / in_regex intrinsic family, whose signatures involve the RegLan sort. RegLan is not a first-class SMT-LIB sort: cvc5 rejects such a declaration with "expected first-class sort as domain sort", so any goto program carrying these intrinsics fails before solving. The applications are lowered inline by convert_expr, so the declaration is not needed at all -- skip it whenever the symbol's mathematical_function_typet involves ID_regex in its domain or codomain.

The existing unit tests never caught this because the get_assert helper strips everything before "(assert ": the ill-sorted declaration was being emitted, unchecked, all along. The new test section checks the FULL output: no "RegLan)" declaration text, and the inline (str.in_re s2 (str.to_re s1)) lowering intact. It fails without the fix and passes with it.

• 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 SMT2 output generation for regex-related intrinsics by preventing emission of uninterpreted-function (declare-fun ...) declarations whose domain/codomain contains CBMC’s ID_regex (SMT-LIB RegLan), which is not a first-class sort and is rejected by cvc5. This fits into CBMC’s SMT2 backend (smt2_convt) and its unit tests by ensuring regex applications are only emitted via the existing inline lowering in convert_expr.

Changes:

• Skip UF declarations in smt2_convt::find_symbols for ID_mathematical_function symbols whose signature includes ID_regex.
• Add a unit test section that checks the full SMT2 output (not just the extracted assert) to ensure no RegLan UF declaration is emitted and that the inline lowering remains intact.

Reviewed changes

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

File	Description
unit/solvers/smt2/smt2_conv.cpp	Adds a unit test that inspects full SMT2 output to ensure no RegLan UF declaration is present and regex lowering is preserved.
src/solvers/smt2/smt2_conv.cpp	Updates find_symbols to avoid declaring UFs with regex/RegLan in their function signature.

---

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.83%. Comparing base (9e80cec) to head (c4fb05c).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9137   +/-   ##
========================================
  Coverage    80.83%   80.83%           
========================================
  Files         1715     1715           
  Lines       189957   190009   +52     
  Branches        73       73           
========================================
+ Hits        153549   153600   +51     
- Misses       36408    36409    +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.