Как реализовать логику AND в Z3Py

Question

Я хочу реализовать ограничение, которое требует логики AND в Z3Py. Предположим, у нас есть две переменные a а также bЯ просто хочу добавить одно ограничение, которое требует a == 0 а также b == 1, Там должно быть несколько способов, которые могут сделать это в Z3, как s.add(a == 0, b == 0) или же s.add(And(a==0, b==0), Тем не менее, я попробовал один метод, который s.add(a == 0 and b == 0), Этот метод не работает, код:

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()

#s.add(a == 0, b ==1)
#s.add(And(a == 0, b == 1))
s.add(a == 0 and b == 1)

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

Выход этого файла a = 0, что означает, что b игнорируется... Может кто-нибудь объяснить, почему это происходит? Похоже на то And(a == 0, b == 1) а также a == 0 and b == 1 отличаются в Z3Py.