Why this works:
>>> from z3 import *
>>> s = Solver()
>>> s.add([True])
>>> s.check()
sat
but this doesn't:
>>> from z3 import *
>>> s = Solver()
>>> s.check([True])
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "$HOME/.local/lib/python3.6/site-packages/z3/z3.py", line 6656, in check
_assumptions[i] = assumptions[i].as_ast()
AttributeError: 'bool' object has no attribute 'as_ast'
>>>
Am I missing something? I understood that it was the same operation but without recording the new constraints into the solver.
I am using Z3 version 4.8.6 - 64 bit
As you are pointing out, there's really no good reason for the treatment of arguments differently here.
Due to the untyped nature of Python, z3 bindings "play" tricks to interpret what you wrote by casting them into various forms it can work with. For the s.add method, they are more "flexible" than the s.check() function.
You can work around it by writing:
>>> from z3 import *
>>> s = Solver()
>>> s.check([Bool(True)])
sat
Note that the same works with s.add too:
>>> from z3 import *
>>> s = Solver()
>>> s.add([Bool(True)])
>>> print(s.check())
sat
So, you can be "consistent" by writing boolean literals in a form that's supported by both add and check. But ideally, the methods themselves should be uniform in their handling of terms. You've found a case where they differ for no good reason.
This isn't necessarily a "bug," as is typical in Python: Lack of static types force library developers to support myriad of cases, and it's hard to keep everything consistent in such a setting. But it definitely is a wart. If it's really causing you trouble, you can report it as such here: https://github.com/Z3Prover/z3/issues to see if there's someone who is concerned enough with this inconsistency to address it. (A pull-request fixing it will most likely be appreciated, the code is here.)