SMT Z3 trace fix

[TGWDB]

This PR fixes parsing of array values in traces from Z3.

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

[codecov]

Codecov Report

Merging #6210 (0d2ccc1) into develop (0a0a862) will decrease coverage by 0.13%.
The diff coverage is 79.06%.

❗ Current head 0d2ccc1 differs from pull request most recent head d125b1a. Consider uploading reports for the commit d125b1a to get more accurate results

@@             Coverage Diff             @@
##           develop    #6210      +/-   ##
===========================================
- Coverage    75.20%   75.06%   -0.14%     
===========================================
  Files         1458     1458              
  Lines       161311   161374      +63     
===========================================
- Hits        121318   121143     -175     
- Misses       39993    40231     +238     

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	95.83% <ø> (ø)
src/goto-programs/goto_convert_class.h	87.30% <ø> (ø)
src/solvers/smt2/smt2_conv.h	100.00% <ø> (ø)
src/solvers/smt2/smt2_dec.h	100.00% <ø> (ø)
src/solvers/smt2/smt2_conv.cpp	66.42% <56.25%> (-0.12%)	⬇️
src/goto-programs/goto_convert.cpp	91.76% <90.00%> (+0.06%)	⬆️
src/goto-instrument/code_contracts.cpp	86.56% <91.11%> (+0.20%)	⬆️
src/solvers/flattening/boolbv.cpp	80.63% <100.00%> (ø)
src/solvers/prop/prop_conv_solver.cpp	88.18% <100.00%> (ø)
src/solvers/smt2/smt2_dec.cpp	71.42% <100.00%> (ø)
... and 19 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3e0007f...d125b1a. Read the comment docs.

[peterschrammel]

I don't see any arrays in these tests. Could you add any tests/checks for the added functionality?

[martin-cs]

Seems OK but 1. can we have a few tests for this and 2. this will probably need cross solver testing as it is not a standardised part of SMT-LIB.

[TGWDB]

Merging this now that there are tests and everything passes. Also noting that this appears to do correct trace output for cvc3 and cvc4 as well, while also improving to some extent output for cprover-smt2 albeit not as well.