Why is Z3 throwing a 'sort mismatch' exception here?

I have the following code:

from z3       import *
x= Bool('x')
State, (A,B) = EnumSort('State',['A', 'B'])
s = Const('s', State)
#s = Int('s')
vars = [s,x]
if x in vars:
    print('yes')

when I run it I get an exception:

Traceback (most recent call last):
  File "/cygdrive/c/temp/testSorts.py", line 9, in <module>
    if x in vars:
  File "/cygdrive/c/ProgramFiles/z3-4.8.12-x64-win/bin/python/z3/z3.py", line 1012, in __eq__
    a, b = _coerce_exprs(self, other)
  File "/cygdrive/c/ProgramFiles/z3-4.8.12-x64-win/bin/python/z3/z3.py", line 1186, in _coerce_exprs
    s = _coerce_expr_merge(s, b)
  File "/cygdrive/c/ProgramFiles/z3-4.8.12-x64-win/bin/python/z3/z3.py", line 1171, in _coerce_expr_merge
    _z3_assert(False, "sort mismatch")
  File "/cygdrive/c/ProgramFiles/z3-4.8.12-x64-win/bin/python/z3/z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: sort mismatch

If I change the type of the variable s from my own sort to a standard one, say Int then everything's fine.

Could someone tell me what I'm missing?

Solution

This is due to the rather "weakly" typed nature of z3-bindings for Python.

SMTLib (and hence z3) is a strongly-typed language: Every variable has a given sort, and it is illegal to even compare two variables that don't have the same sort. (i.e., it's a type error.)

For various (both historical and technical) reasons, Python API blurs the boundaries of types: It tries to cast them as appropriate to make things work, to follow the Python philosophy of untyped programming. Unfortunately, this is one of those cases where it doesn't work, and the outcome is utterly confusing: When you compare an Int and a Bool, there's an internal check to return false; but there isn't such a check when you have an enumerated type. Hence the error you're getting.

So, how do you program when you need such checks? Always check the sort first. So, you should code that if-statement as:

for v in vars:
    if (x.sort() == v.sort()) and (x == v):
        print('yes')

You'll see that this version works correctly regardless whether s is an enumeration sort, or Bool, or some other type. It's more verbose than what you wrote, but it's the only way to code such things without falling to the traps of weakly-typed nature of the python API for z3.