zstring: fix encode rountrip for '\' as printable ASCII (#5120)

This fixes encode roundtripping for all printable ASCII characters.
In particular, this now leaves a plain '\' untouched by the
encoding logic, instead of converting it to escaped hex-digits.
It also adds unit testing covering this specific zstring encoding
property, in order to avoid future regressions.

src/test/CMakeLists.txt

@@ -129,6 +129,7 @@ add_executable(test-z3
   vector.cpp
   lp/lp.cpp
   lp/nla_solver_test.cpp
+  zstring.cpp
   ${z3_test_extra_object_files}
 )
 z3_add_install_tactic_rule(${z3_test_deps})