Unknown when working with String Sequences

[manojlds]

I am trying to work with sequences (modeling SQL conditions, and need it to work with IN clauses of the form "US" in ImportCountries to see if two conditions can be True at the same time):

s = Solver()
test = Const('test', SeqSort(StringSort()))

expr1 = Contains(test, Unit(StringVal("US")))
expr2 = Not(Contains(test, Unit(StringVal("AE"))))

s.add(And(expr1 == True, expr2 == True))

print(s.check()) # Gives unknown.

Doing the same with Int sequence works as expected.

s = Solver()

test = Const('test', SeqSort(IntSort()))

expr1 = Contains(test, Unit(IntVal(1)))
expr2 = Not(Contains(test, Unit(IntVal(2))))

s.add(And(expr1 == True, expr2 == True))

print(s.check())
print(s.model())

I asked the question on StackOverflow and someone was able to replicate this issue with Z3 but the same equivalent works as expected in CVC5 - https://stackoverflow.com/a/78104548/526535