z3py's Solver.check does not accept assumptions

[Vlad-Shcherbina]

>>> import z3
>>> solver = z3.Solver()
>>> x = z3.Int('x')
>>> solver.add(x == 0)
>>> solver.check()  # works
sat
>>> solver.check(x == 0)  # fails
WARNING: an assumption must be a propositional variable or the negation of one
unknown

I observed it both in binary release of 4.3.2 on windows with python 2.7 and in recent linux build of unstable branch at 6c1a539 with python 3.4.

[NikolajBjorner]

Assumptions can only be propositional variables. So you have to create a propositional variable that is shorthand for the formula you assume.

from z3 import *
solver = z3.Solver()
x = z3.Int('x')
p = z3.Bool('p')
solver.add((x == 0) == p)
solver.check(p)