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.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.