Enable pointer tests from regression/cbmc to run using new SMT backend.

[NlightNFotis]

This PR enables extra tests from the regression/cbmc folder, targeting
pointers, so that we can gauge our current level of support for pointers
in the new SMT backend.

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

[NlightNFotis]

While working on this PR, a number of tests were failing (nearly all of them because of unimplemented features):

• Pointer_Arithmetic1 - unimplemented: array
• Pointer_Arithmetic11 - unimplemented: byte_extract_little_endian
• Pointer_Arithmetic16 - unimplemented: array
• Pointer_Arithmetic8 - unimplemented: array
• Pointer24 - flips verification result from success to failure
  • Inconsistent with SAT backend, but consistent with old SMT backend
  • Marked broken-smt-backend
• Pointer20 - unimplemented: nondet_symbol
• Pointer21 - unimplemented: struct_tag
  • Marked broken-smt-backend
• Pointer23 - unimplemented: is_invalid_pointer
• Pointer28 - unimplemented: array
• Pointer3 - unimplemented: array
• Pointer4 - unimplemented: nondet_symbol
• Pointer_array1 - unimplemented: struct_tag
• Pointer_array2 - unimplemented: struct_tag
• Pointer_array3 - unimplemented: array
• Pointer_array4 - unimplemented: array
• Pointer_array6 - unimplemented: nondet_symbol
• Pointer_byte_extract2 - unimplemented: byte_extract_little_endian
• Pointer_byte_extract4 - unimplemented: struct_tag
• Pointer_byte_extract5 - unimplemented: array
• Pointer_comparison2 - unimplemented: array
• Pointer_comparison3 - unimplemented: nondet_symbol
• Pointer_difference1 - unimplemented: array
• pointer-primitive-check-01 - unimplemented: is_invalid_pointer
• pointer-primitive-check-03 - unimplemented: nondet_symbol
• pointer-primitive-check-04 - unimplemented: is_invalid_pointer

[codecov]

Codecov Report

Merging #6910 (272ebfd) into develop (5c7fb76) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6910   +/-   ##
========================================
  Coverage    77.78%   77.79%           
========================================
  Files         1568     1568           
  Lines       180269   180301   +32     
========================================
+ Hits        140230   140265   +35     
+ Misses       40039    40036    -3     

Impacted Files	Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	88.32% <100.00%> (+0.62%)	⬆️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	99.66% <100.00%> (+0.01%)	⬆️

---

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 f73a1a0...272ebfd. Read the comment docs.

[TGWDB]

Approved assuming the PR it is based on goes through fine.

It would nice to have the information from your comment somewhere else, I guess it will be lost (or at least not easily found and looked at) when the PR is merged.