diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index 241c991f6..b6e024aff 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -554,138 +554,6 @@ def testBasicMigration(self):
 
         self.assertItemsEqual(solver.get_all_values(cs1, var1), [2])  # should only be [2]
 
-    def test_ORD(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        cs.add(Operators.ORD(a) == Operators.ORD("Z"))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), ord("Z"))
-
-    def test_CHR(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        cs.add(Operators.CHR(a) == Operators.CHR(0x41))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), 0x41)
-
-    def test_CONCAT(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(16)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-
-        cs.add(b == 0x41)
-        cs.add(c == 0x42)
-        cs.add(a == Operators.CONCAT(a.size, b, c))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), Operators.CONCAT(a.size, 0x41, 0x42))
-
-    def test_ITEBV_1(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-
-        cs.add(b == 0x41)
-        cs.add(c == 0x42)
-        cs.add(a == Operators.ITEBV(8, b == c, b, c))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), 0x42)
-
-    def test_ITEBV_2(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-
-        cs.add(b == 0x44)
-        cs.add(c == 0x44)
-        cs.add(a == Operators.ITEBV(8, b == c, b, c))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), 0x44)
-
-    def test_ITE(self):
-        cs = ConstraintSet()
-        a = cs.new_bool()
-        b = cs.new_bool()
-        c = cs.new_bool()
-
-        cs.add(b == True)
-        cs.add(c == False)
-        cs.add(a == Operators.ITE(b == c, b, c))
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), False)
-
-    def test_UREM(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-        d = cs.new_bitvec(8)
-
-        cs.add(b == 0x86)  # 134
-        cs.add(c == 0x11)  # 17
-        cs.add(a == Operators.UREM(b, c))
-        cs.add(d == b.urem(c))
-        cs.add(a == d)
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), 0xF)
-
-    def test_SREM(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-        d = cs.new_bitvec(8)
-
-        cs.add(b == 0x86)  # -122
-        cs.add(c == 0x11)  # 17
-        cs.add(a == Operators.SREM(b, c))
-        cs.add(d == b.srem(c))
-        cs.add(a == d)
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), -3 & 0xFF)
-
-    def test_UDIV(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-        d = cs.new_bitvec(8)
-
-        cs.add(b == 0x86)  # 134
-        cs.add(c == 0x11)  # 17
-        cs.add(a == Operators.UDIV(b, c))
-        cs.add(d == b.udiv(c))
-        cs.add(a == d)
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), 7)
-
-    def test_SDIV(self):
-        cs = ConstraintSet()
-        a = cs.new_bitvec(8)
-        b = cs.new_bitvec(8)
-        c = cs.new_bitvec(8)
-        d = cs.new_bitvec(8)
-
-        cs.add(b == 0x86)  # -122
-        cs.add(c == 0x11)  # 17
-        cs.add(a == Operators.SDIV(b, c))
-        cs.add(d == b // c)
-        cs.add(a == d)
-
-        self.assertTrue(solver.check(cs))
-        self.assertEqual(solver.get_value(cs, a), -7 & 0xFF)
-
     def test_SAR(self):
         solver = Z3Solver.instance()
         A = 0xBADF00D