Produce annotated pointer constants in incremental SMT2 traces

[tautschnig]

When the incremental SMT2 decision procedure returns pointer values via get(), it now creates annotated_pointer_constant_exprt instead of plain constant_exprt. This enables the trace printer to display symbolic pointer expressions (like string literals and address-of expressions) instead of raw integer addresses.

The pointer bit-vector is decomposed into object ID (high bits) and offset (low bits) using config.bv_encoding.object_bits. The object ID is looked up in the decision procedure's object_map to find the base expression, and get_subexpression_at_offset is used to construct the symbolic pointer, following the same approach as the SAT backend's pointer_logict::pointer_expr.

A new overload of construct_value_expr_from_smt accepts the smt_object_mapt. The original overload without the object map continues to work unchanged for backward compatibility.

Removes the no-new-smt tag from three regression tests that now pass with the incremental SMT2 backend: trace-strings,
trace_address_arithmetic1, and xml-trace2.

When string constants or other expressions are substituted with symbol_exprt identifiers during SMT conversion, the object_map tracks the substituted symbol rather than the original expression. This caused pointer values in traces to display as 'array_0' instead of the original string literal like '"abc"'.

Add expression_identifiers parameter to construct_value_expr_from_smt to enable reverse lookup from substituted symbol names back to original expressions. In build_annotated_pointer, when the base expression from the object_map is a symbol_exprt, check if it matches any identifier in expression_identifiers and use the original expression for the symbolic pointer display.

Passes all 170 smt2_incremental unit tests (1040 assertions) and the trace-strings, trace_address_arithmetic1, and xml-trace2 regression tests with both SAT and incremental SMT2 backends.

When get_subexpression_at_offset fails, return nil_exprt{} instead of a default-constructed exprt{} so that the is_nil() check in build_annotated_pointer correctly detects the failure and falls back to a plain constant_exprt.

Fixes: #8067

• Each commit message has a non-empty body, explaining why the change was made.
• 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 improves trace readability for the incremental SMT2 backend by reconstructing symbolic pointer expressions (e.g., string literals / address-of expressions) when decoding pointer values returned by SMT get-value, instead of always emitting raw bitvector constants.

Changes:

• Add construct_value_expr_from_smt overloads that accept the incremental SMT2 decision procedure’s object_map, and optionally expression_identifiers, to build annotated_pointer_constant_exprt for pointer-typed values.
• Update smt2_incremental_decision_proceduret::get_expr to use the new overload so pointer values in traces can be printed symbolically.
• Enable the incremental SMT2 backend for three trace-related CBMC regression tests by removing the no-new-smt tag.

Reviewed changes

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

Show a summary per file

File	Description
src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp	Reconstruct annotated pointer constants using object id/offset decoding, and optionally reverse identifier substitutions.
src/solvers/smt2_incremental/construct_value_expr_from_smt.h	Expose new overloads for annotated-pointer reconstruction.
src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp	Route get-value decoding through the new overload with object/expression maps.
unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp	Add unit tests for annotated pointer construction and reverse substitution lookup.
regression/cbmc/xml-trace2/test.desc	Remove no-new-smt marker now that incremental backend supports the expected trace output.
regression/cbmc/trace-strings/test.desc	Remove no-new-smt marker now that incremental backend supports the expected trace output.
regression/cbmc/trace_address_arithmetic1/test.desc	Remove no-new-smt marker now that incremental backend supports the expected trace output.

---

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

[codecov]

Codecov Report

❌ Patch coverage is 96.69811% with 7 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.49%. Comparing base (803f904) to head (9146723).
⚠️ Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
...smt2_incremental/construct_value_expr_from_smt.cpp	96.22%	4 Missing ⚠️
...smt2_incremental/construct_value_expr_from_smt.cpp	97.08%	3 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8901      +/-   ##
===========================================
+ Coverage    80.47%   80.49%   +0.01%     
===========================================
  Files         1704     1704              
  Lines       188694   188904     +210     
  Branches        73       73              
===========================================
+ Hits        151843   152049     +206     
- Misses       36851    36855       +4     

☔ View full report in Codecov by Sentry.
📢 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.