title: Or of bitvectors in z3Py
body: <p>Ideally it is possible to 'Or' two numbers represented as bitvectors but I am not able to it. Please tell if there is some error in the code or something else</p>
  
  <pre><code>line1 = BitVec('line1', 1)
  line2 = BitVec('line2', 1)
  s = Solver()
  s.add(Or(line1, line2) == 0)
  print s.check()
  </code></pre>
  
  <p>The error given is</p>
  
  <pre><code>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)
  </code></pre>
  
  <p>From this error I understand that Or can be done only for bool variables. My question is how to Or for BitVectors</p>