Push empty-type equality short-circuit into convert_expr_to_smt

[tautschnig]

Builds upon #8907.

Previously, equality of two zero-width-typed (typically void) operands was handled at the top level of smt2_incremental_decision_proceduret::set_to: the equal_exprt was matched textually before lowering reached convert_expr_to_smt, and a dedicated branch emitted either nothing (for value == true) or (assert false) (for value == false). This worked for the common case but failed for nested shapes such as

set_to(and_exprt{equal_exprt{x_void, y_void}, other}, true)

because the recursive visitor in convert_expr_to_smt would still descend into the void operands of the inner equal_exprt and trip UNIMPLEMENTED_FEATURE in convert_type_to_smt_sort(empty_typet).

Move the short-circuit one layer down, into convert_expr_to_smt:

• Add a const namespacet & parameter to the public convert_expr_to_smt and propagate it to the dispatcher and to the equal_exprt overload.
• In the entry-point's filtered_visit_post filter, return false for an equal_exprt whose operands have zero-width type, so that the visitor does not descend into the void operands and does not attempt convert_type_to_smt_sort on them.
• In the equal_exprt overload of convert_expr_to_smt, return smt_bool_literal_termt{true} directly when the operand type is zero-width, mirroring smt2_conv.cpp:1604 (convert_expr(true_exprt())).
• Drop the now-redundant top-level short-circuit from set_to: convert_expr_to_smt produces the boolean literal true, which set_to asserts as-is for value == true and negates for value == false. This means the SMT output for the trivial top-level case becomes (assert true) / (assert (not true)) rather than nothing / (assert false). Both are semantically equivalent and match the end-to-end behaviour of the non-incremental SMT2 backend.

The gather-side filter in gather_dependent_expressions is kept: it is a separate walk that runs before the convert-side visitor and still needs to skip zero-width-typed leaves to avoid sending declare-fun for them (which would also call convert_type_to_smt_sort on an empty type).

Update the unit test for set_to over empty type to reflect the new SMT command sequence, and add a new unit test set_to over nested empty-type equality that exercises the nested shape (an and_exprt whose lhs is an empty-type equal_exprt). The existing getting value of empty struct test, which uses empty structs (lowered to bv_typet{8} via struct_encoding) rather than true void, continues to pass unchanged.

Co-authored-by: Kiro kiro-agent@users.noreply.github.com

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