diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py
index 527ec381..9a78374b 100644
--- a/mythril/laser/smt/bitvec.py
+++ b/mythril/laser/smt/bitvec.py
@@ -23,6 +23,30 @@ class BitVec(Expression):
         union = self.annotations + other.annotations
         return BitVec(self.raw / other.raw, annotations=union)
 
+    def __and__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw & other.raw, annotations=union)
+
+    def __or__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw | other.raw, annotations=union)
+
+    def __xor__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw ^ other.raw, annotations=union)
+
+
+def Concat(*args):
+    nraw = z3.Concat([a.raw for a in args])
+    annotations = []
+    for bv in args:
+        annotations += bv.annotations
+    BitVec(nraw, annotations)
+
+
+def Extract(high, low, bv: BitVec):
+    BitVec(z3.Extract(high, low, bv.raw), annotations=bv.annotations)
+
 
 def URem(a: BitVec, b: BitVec) -> BitVec:
     union = a.annotations + b.annotations
@@ -39,6 +63,11 @@ def UDiv(a: BitVec, b: BitVec) -> BitVec:
     return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
 
 
+def UDiv(a: BitVec, b: BitVec) -> BitVec:
+    union = a.annotations + b.annotations
+    return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
+
+
 def BitVecVal(value, size, annotations=None):
     raw = z3.BitVecVal(value, size)
     return BitVec(raw, annotations)