Possible regression in model output for functions from strings to strings in python

[ahelwer]

A user claims here this is not an issue in the 08/03/2021 build of Z3 but is an issue in the 11/15/2021 build. However, I have reproduced this issue on both 4.8.12 (released 07/13/2021) and 4.8.13 (released 11/18/2021). I am running on Windows 11 with Python 3.9.6. The issue is as follows; given the following python program:

from z3 import *
map = Function('map', StringSort(), StringSort())
c1 = map(StringVal('key1')) == StringVal('value1')
c2 = map(StringVal('key2')) == StringVal('value2')
c3 = map(StringVal('key3')) == StringVal('value3')
c4 = map(StringVal('key4')) == StringVal('value4')
s = Solver()
s.add(And(c1, c2, c3, c4))
print(s.check())
print(s.model())

we expect the output model to look like the following:

[map = ["key2" -> "value2",
        "key3" -> "value3",
        "key4" -> "value4",
        else -> "value1"]]

but actually it looks like:

[map = [Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value1",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value2",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value3",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value4",
        else -> "value1"]]