Yes, Or(a,b)
is a boolean disjunction, you probably want a bitwise or since you're trying to compare bitvectors, which can be done in the Python API using |
from the documentation (here's a z3py link for the example: http://rise4fun.com/Z3Py/1l0):
line1 = BitVec('line1', 2)
line2 = BitVec('line2', 2)
s = Solver()
P = (line1 | line2) != 0
print P
s.add(P)
print s.check()
print s.model() # [line2 = 0, line1 = 3]
I updated your example so that line1 and line2 are longer than 1 bit (which would be equivalent to the boolean case, but is a different type, hence the error).
Note that this is bvor
in the SMT-LIB standard, see http://smtlib.cs.uiowa.edu/logics/V1/QF_BV.smt