python - またはz3Pyのビットベクトルの

Question

理想的には、ビットベクトルとして表される 2 つの数値を「論理和」することが可能ですが、私にはできません。コードにエラーがあるかどうか教えてください。

line1 = BitVec('line1', 1)
line2 = BitVec('line2', 1)
s = Solver()
s.add(Or(line1, line2) == 0)
print s.check()

与えられたエラーは

error: 'type error'
WARNING: invalid function application for or, sort mismatch on argument at position 1,         expected Bool but given (_ BitVec 1)
WARNING: (declare-fun or (Bool Bool) Bool) applied to: 
line1 of sort (_ BitVec 1)
line2 of sort (_ BitVec 1)

このエラーから、Or は bool 変数に対してのみ実行できることがわかりました。私の質問は、または BitVectors の方法です