Add support for union values in traces for incremental smt2 decision procedure

[thomasspriggs]

This PR adds support for union values in traces for incremental smt2 decision procedure.

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

[esteffin]

❓ Why only the first component?
What about the others?

[thomasspriggs]

This matches the SAT backend. I should add a comment to that effect. The return expression is a union_exprt which only supports a single member, which makes sense as they could otherwise be in conflict. There are other things we could potentially do or return, but I wanted to aim for consistency; at least initially.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (f9f8cde) 78.14% compared to head (8d8dfa9) 78.98%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7990      +/-   ##
===========================================
+ Coverage    78.14%   78.98%   +0.83%     
===========================================
  Files         1701     1701              
  Lines       196386   196458      +72     
===========================================
+ Hits        153475   155170    +1695     
+ Misses       42911    41288    -1623     

Files	Coverage Δ
...vers/smt2_incremental/encoding/struct_encoding.cpp	97.24% <100.00%> (+0.27%)	⬆️
...olvers/smt2_incremental/encoding/struct_encoding.h	100.00% <ø> (ø)
...ncremental/smt2_incremental_decision_procedure.cpp	95.97% <100.00%> (+0.08%)	⬆️
..._incremental/smt2_incremental_decision_procedure.h	75.00% <ø> (ø)
...vers/smt2_incremental/encoding/struct_encoding.cpp	100.00% <100.00%> (ø)
...ncremental/smt2_incremental_decision_procedure.cpp	99.01% <100.00%> (+0.01%)	⬆️

... and 58 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.