Support for printing strings in traces is not yet implemented for the incremental smt2 decision procedure #8067
Description
Support for printing strings in traces is not yet implemented for the incremental smt2 decision procedure. We support solving inputs containing string literals by encoding them into array theory. As C-strings are normally tracked char * pointers, the trace generation is looking for the values of these pointers. Currently using the new SMT decision procedure results in these being displayed as the pointer addresses. Running with the SAT based decision procedure results in the string literals being printed, rather than the address.
This issue affects the following regression tests -
- cbmc/trace_address_arithmetic1/test.desc
- cbmc/trace-strings/test.desc
- cbmc/xml-trace2/test.desc