#7151·z3

Unknown when working with String Sequences

Author: manojldsCreated Mar 6, 2024Updated Jul 13, 2026

Labelsstring

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):

python

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.

python

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

Source: Z3Prover/z3

View original on GitHub View discussion on GitHub